OAI/Computability/PerfectCompleteness/Foundations/CanonicalKeys.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.CanonicalKeys.Side line 14
  2. structure OAI.PerfectCompleteness.CanonicalKeys.Key line 19
  3. def OAI.PerfectCompleteness.CanonicalKeys.partition line 24
  4. def OAI.PerfectCompleteness.CanonicalKeys.key line 28
  5. theorem OAI.PerfectCompleteness.CanonicalKeys.constantOnFibers line 32
  6. theorem OAI.PerfectCompleteness.CanonicalKeys.covered_iff_legal line 37
  7. theorem OAI.PerfectCompleteness.CanonicalKeys.legal_domain_projection line 44
  8. theorem OAI.PerfectCompleteness.CanonicalKeys.partition_projection line 50
  9. theorem OAI.PerfectCompleteness.CanonicalKeys.key_projection line 58
  10. abbrev OAI.PerfectCompleteness.CanonicalKeys.Label line 63
  11. def OAI.PerfectCompleteness.CanonicalKeys.evaluateLabel line 66
  12. def OAI.PerfectCompleteness.CanonicalKeys.restore line 70
  13. theorem OAI.PerfectCompleteness.CanonicalKeys.restore_evaluateLabel line 74
  14. theorem OAI.PerfectCompleteness.CanonicalKeys.restore_injective line 79
  15. def OAI.PerfectCompleteness.CanonicalKeys.transportLabel line 83
  16. theorem OAI.PerfectCompleteness.CanonicalKeys.transportLabel_bijective line 91
  17. theorem OAI.PerfectCompleteness.CanonicalKeys.evaluateLabel_projection line 103
  18. theorem OAI.PerfectCompleteness.CanonicalKeys.restore_projection line 114