OAI/Computability/PerfectCompleteness/Repetition/StoppedCleanGeometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.StoppedCleanGeometry.descendant line 22
  2. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.lowerNode_descendant line 31
  3. def OAI.PerfectCompleteness.StoppedCleanGeometry.cut line 43
  4. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.lowerHeight line 49
  5. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.fullPath_spec line 54
  6. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.append_cast_heq line 68
  7. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.cleanPath_eq line 74
  8. def OAI.PerfectCompleteness.StoppedCleanGeometry.firstLeaf line 83
  9. abbrev OAI.PerfectCompleteness.StoppedCleanGeometry.OutsideQuestions line 94
  10. def OAI.PerfectCompleteness.StoppedCleanGeometry.fixedOutside line 98
  11. def OAI.PerfectCompleteness.StoppedCleanGeometry.placeholder line 103
  12. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.fixedOutside_at line 107
  13. abbrev OAI.PerfectCompleteness.StoppedCleanGeometry.Exterior line 116
  14. def OAI.PerfectCompleteness.StoppedCleanGeometry.filledExteriorEquiv line 122
  15. def OAI.PerfectCompleteness.StoppedCleanGeometry.exteriorEquiv line 134
  16. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.exteriorEquiv_law line 146
  17. def OAI.PerfectCompleteness.StoppedCleanGeometry.geometry line 152
  18. theorem OAI.PerfectCompleteness.StoppedCleanGeometry.geometry_path line 161