OAI/Computability/PerfectCompleteness/Foundations/QuotientTableAgreementLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.QuotientTableAgreement.projectedAgreement line 27
  2. theorem OAI.PerfectCompleteness.QuotientTableAgreement.projectedAgreement_eq line 34
  3. theorem OAI.PerfectCompleteness.QuotientTableAgreement.projectedAgreement_eq_nonzeroAgreement line 44
  4. theorem OAI.PerfectCompleteness.MixedSupport.localKey_kernel_invariant line 62
  5. theorem OAI.PerfectCompleteness.MixedSupport.localReduction_kernel_invariant line 77
  6. theorem OAI.PerfectCompleteness.MixedSupport.sectionFunction_kernel_invariant line 95
  7. theorem OAI.PerfectCompleteness.MixedSupport.keyFields_kernel_invariant line 104
  8. theorem OAI.PerfectCompleteness.MixedSupport.coordinateReduction_kernel_invariant line 113
  9. theorem OAI.PerfectCompleteness.MixedSupport.reduction_kernel_invariant line 122
  10. theorem OAI.PerfectCompleteness.MixedSupport.retainedKeys_kernel_invariant line 129
  11. theorem OAI.PerfectCompleteness.ReducedPartition.fiber_kernel_invariant line 141
  12. theorem OAI.PerfectCompleteness.ReducedPartition.parts_kernel_invariant line 151
  13. theorem OAI.PerfectCompleteness.MixedSupport.reducedParts_kernel_invariant line 165
  14. theorem OAI.PerfectCompleteness.CanonicalKeys.partition_kernel_invariant line 185
  15. theorem OAI.PerfectCompleteness.CanonicalKeys.key_kernel_invariant line 191
  16. theorem OAI.PerfectCompleteness.CanonicalKeys.key_postcomp_injective line 198
  17. theorem OAI.PerfectCompleteness.CanonicalKeys.key_postcomp_equiv line 205
  18. def OAI.PerfectCompleteness.CanonicalKeys.transportKernel line 210
  19. theorem OAI.PerfectCompleteness.CanonicalKeys.transportKernel_bijective line 219
  20. theorem OAI.PerfectCompleteness.CanonicalKeys.transportKernel_evaluateLabel line 232
  21. theorem OAI.PerfectCompleteness.CanonicalKeys.restore_transportKernel line 243
  22. abbrev OAI.PerfectCompleteness.KeyStrategy.NonemptyKey line 266
  23. abbrev OAI.PerfectCompleteness.KeyStrategy.Strategy line 268
  24. def OAI.PerfectCompleteness.KeyStrategy.queryKey line 273
  25. def OAI.PerfectCompleteness.KeyStrategy.label line 279
  26. def OAI.PerfectCompleteness.KeyStrategy.response line 283
  27. theorem OAI.PerfectCompleteness.KeyStrategy.response_mem_range line 287
  28. theorem OAI.PerfectCompleteness.KeyStrategy.label_val_eq_of_key_eq line 291
  29. theorem OAI.PerfectCompleteness.KeyStrategy.response_postcomp_injective line 298
  30. theorem OAI.PerfectCompleteness.KeyStrategy.response_projection line 314
  31. def OAI.PerfectCompleteness.KeyStrategy.extend line 326
  32. theorem OAI.PerfectCompleteness.KeyStrategy.extend_val line 332