OAI/Computability/PerfectCompleteness/Foundations/CanonicalCoarseningErasure.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.CanonicalCoarseningErasure.transportLabel line 16
  2. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.transportLabel_val line 23
  3. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.transportLabel_bijective line 26
  4. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.transportLabel_evaluateLabel line 39
  5. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.restore_transportLabel line 50
  6. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.coarsen_transportLabel line 62
  7. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.coarsen_val line 80
  8. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.partIndex_transportLabel line 87
  9. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.partIndex_coarsen line 92
  10. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.labelIndex_transportLabel line 100
  11. theorem OAI.PerfectCompleteness.CanonicalCoarseningErasure.labelIndex_coarsen line 106