OAI/Computability/PerfectCompleteness/Foundations/GeometricPathLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.GeometricPath.leafPath line 19
  2. theorem OAI.PerfectCompleteness.GeometricPath.leafPath_endpoint line 23
  3. def OAI.PerfectCompleteness.GeometricPath.nodeAtLevel line 32
  4. theorem OAI.PerfectCompleteness.GeometricPath.nodeAtLevel_last line 37
  5. theorem OAI.PerfectCompleteness.GeometricPath.nodeAtLevel_castSucc line 43
  6. theorem OAI.PerfectCompleteness.GeometricPath.nodeAtLevel_height line 51
  7. theorem OAI.PerfectCompleteness.GeometricPath.nodeAtLevel_injective line 63
  8. theorem OAI.PerfectCompleteness.GeometricPath.slots_nonempty line 71
  9. def OAI.PerfectCompleteness.GeometricPath.law line 80
  10. theorem OAI.PerfectCompleteness.GeometricPath.law_step line 85
  11. def OAI.PerfectCompleteness.HierarchicalKnownRows.lower line 114
  12. theorem OAI.PerfectCompleteness.HierarchicalKnownRows.lower_apply line 118
  13. def OAI.PerfectCompleteness.HierarchicalKnownRows.knownSpace line 124
  14. theorem OAI.PerfectCompleteness.HierarchicalKnownRows.one_mem_knownSpace line 127
  15. theorem OAI.PerfectCompleteness.HierarchicalKnownRows.product_mem_knownSpace line 131
  16. theorem OAI.PerfectCompleteness.HierarchicalKnownRows.knownSpace_le_factoringSpace line 140
  17. theorem OAI.PerfectCompleteness.HierarchicalKnownRows.determined line 150