OAI/Computability/PerfectCompleteness/Foundations/CanonicalEdgesLemmas.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalEdges.coarsen line 16
  2. theorem OAI.PerfectCompleteness.CanonicalEdges.restore_coarsen line 20
  3. theorem OAI.PerfectCompleteness.CanonicalEdges.coarsen_eq_iff line 26
  4. theorem OAI.PerfectCompleteness.CanonicalEdges.coarsen_evaluateLabel line 36
  5. theorem OAI.PerfectCompleteness.CanonicalEdges.coarsen_surjective line 43
  6. theorem OAI.PerfectCompleteness.CanonicalEdges.card_coarsen_fiber_le line 51
  7. theorem OAI.PerfectCompleteness.CanonicalEdges.coarsen_at_most_two line 64
  8. theorem OAI.PerfectCompleteness.CanonicalEdges.binaryDeletion_at_most_two line 70
  9. theorem OAI.PerfectCompleteness.CanonicalEdges.coarsen_transportLabel line 77
  10. inductive OAI.PerfectCompleteness.CanonicalKeyShape.Shape line 109
  11. def OAI.PerfectCompleteness.CanonicalKeyShape.erase line 114
  12. def OAI.PerfectCompleteness.CanonicalKeyShape.dummy line 118
  13. theorem OAI.PerfectCompleteness.CanonicalKeyShape.erase_dummy line 122
  14. def OAI.PerfectCompleteness.CanonicalKeyShape.domainEquiv line 125
  15. instance OAI.PerfectCompleteness.CanonicalKeyShape.dummyDomainFintype line 128
  16. def OAI.PerfectCompleteness.CanonicalKeyShape.shape line 131
  17. def OAI.PerfectCompleteness.CanonicalKeyShape.dummySlots line 133
  18. instance OAI.PerfectCompleteness.CanonicalKeyShape.dummyAssignmentFintype line 135
  19. def OAI.PerfectCompleteness.CanonicalKeyShape.assignmentEquiv line 140
  20. theorem OAI.PerfectCompleteness.CanonicalKeyShape.assignmentEquiv_apply line 147
  21. def OAI.PerfectCompleteness.CanonicalKeyShape.transport line 151
  22. theorem OAI.PerfectCompleteness.CanonicalKeyShape.transport_apply line 154
  23. theorem OAI.PerfectCompleteness.CanonicalKeyShape.assignmentEquiv_update line 159
  24. theorem OAI.PerfectCompleteness.CanonicalKeyShape.sectionFunction_erasure line 166
  25. theorem OAI.PerfectCompleteness.CanonicalKeyShape.localReduction_erasure line 177
  26. theorem OAI.PerfectCompleteness.CanonicalKeyShape.reduction_erasure line 188
  27. theorem OAI.PerfectCompleteness.CanonicalKeyShape.partition_erasure line 199
  28. inductive OAI.PerfectCompleteness.CanonicalKeyShape.SupportMode line 209
  29. def OAI.PerfectCompleteness.CanonicalKeyShape.mode line 216
  30. def OAI.PerfectCompleteness.CanonicalKeyShape.recover line 225
  31. theorem OAI.PerfectCompleteness.CanonicalKeyShape.localKey_recover line 231
  32. theorem OAI.PerfectCompleteness.CanonicalKeyShape.mode_erasure line 243
  33. def OAI.PerfectCompleteness.CanonicalKeyShape.modes line 262
  34. theorem OAI.PerfectCompleteness.CanonicalKeyShape.modes_erasure line 266
  35. theorem OAI.PerfectCompleteness.CanonicalKeyShape.keyFields_recover line 276
  36. def OAI.PerfectCompleteness.CanonicalKeyShape.retained line 287
  37. theorem OAI.PerfectCompleteness.CanonicalKeyShape.retainedKeys_recover line 292
  38. abbrev OAI.PerfectCompleteness.CanonicalKeyShape.Input line 298
  39. instance OAI.PerfectCompleteness.CanonicalKeyShape.inputFintype line 301
  40. def OAI.PerfectCompleteness.CanonicalKeyShape.input line 305
  41. def OAI.PerfectCompleteness.CanonicalKeyShape.inputPartition line 308
  42. def OAI.PerfectCompleteness.CanonicalKeyShape.inputModes line 312
  43. theorem OAI.PerfectCompleteness.CanonicalKeyShape.inputPartition_eq line 315
  44. theorem OAI.PerfectCompleteness.CanonicalKeyShape.inputModes_recover line 320
  45. inductive OAI.PerfectCompleteness.SourceKeys.Endpoint line 338
  46. def OAI.PerfectCompleteness.SourceKeys.slot line 343
  47. inductive OAI.PerfectCompleteness.SourceKeys.Step line 347
  48. def OAI.PerfectCompleteness.SourceKeys.Step.projection line 353
  49. def OAI.PerfectCompleteness.SourceKeys.stepProjection line 358
  50. theorem OAI.PerfectCompleteness.SourceKeys.key_step line 363
  51. def OAI.PerfectCompleteness.SourceKeys.endpointValue line 371
  52. theorem OAI.PerfectCompleteness.SourceKeys.coordinate_restrict line 380
  53. theorem OAI.PerfectCompleteness.SourceKeys.endpointValue_projection line 388
  54. def OAI.PerfectCompleteness.SourceKeys.realizingAssignment line 397
  55. theorem OAI.PerfectCompleteness.SourceKeys.realizingAssignment_projection line 402
  56. theorem OAI.PerfectCompleteness.SourceKeys.evaluated_label_step line 411
  57. theorem OAI.PerfectCompleteness.SourceKeys.evaluated_label_satisfies line 427