OAI/Computability/PerfectCompleteness/Foundations/CanonicalDirections.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.CanonicalDirections.Tuple line 20
  2. def OAI.PerfectCompleteness.CanonicalDirections.directionEquiv line 23
  3. def OAI.PerfectCompleteness.CanonicalDirections.tupleEquiv line 29
  4. theorem OAI.PerfectCompleteness.CanonicalDirections.tupleEquiv_apply line 33
  5. theorem OAI.PerfectCompleteness.CanonicalDirections.tupleEquiv_symm_apply line 37
  6. def OAI.PerfectCompleteness.CanonicalDirections.levelLaw line 42
  7. def OAI.PerfectCompleteness.CanonicalDirections.law line 47
  8. theorem OAI.PerfectCompleteness.CanonicalDirections.directionLaw_toCanonical line 51
  9. theorem OAI.PerfectCompleteness.CanonicalDirections.directionsLaw_toCanonical line 67
  10. theorem OAI.PerfectCompleteness.CanonicalDirections.canonicalLaw_toDirections line 79
  11. theorem OAI.PerfectCompleteness.CanonicalDirections.choiceAt_toCanonical line 94
  12. theorem OAI.PerfectCompleteness.CanonicalDirections.win_eq_observe_canonical line 104
  13. theorem OAI.PerfectCompleteness.CanonicalDirections.win_eq_observe line 115