OAI/Combinatorics/TriangleRemoval/Process/PathForest.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.PathForest line 16
  2. instance OAI.SharpTerminalLeave.PathForest.(instance at line 22) line 22
  3. instance OAI.SharpTerminalLeave.PathForest.(instance at line 26) line 26
  4. def OAI.SharpTerminalLeave.PathForest.parent line 28
  5. def OAI.SharpTerminalLeave.PathForest.Step line 30
  6. def OAI.SharpTerminalLeave.PathForest.Ancestor line 32
  7. def OAI.SharpTerminalLeave.PathForest.OnPath line 34
  8. lemma OAI.SharpTerminalLeave.PathForest.step_lt line 37
  9. lemma OAI.SharpTerminalLeave.PathForest.ancestor_le line 39
  10. lemma OAI.SharpTerminalLeave.PathForest.predecessor_unique line 44
  11. lemma OAI.SharpTerminalLeave.PathForest.ancestor_eq_or_predecessor line 47
  12. lemma OAI.SharpTerminalLeave.PathForest.ancestors_comparable line 53
  13. lemma OAI.SharpTerminalLeave.PathForest.onPath_ancestor line 65
  14. lemma OAI.SharpTerminalLeave.PathForest.onPath_comparable line 70
  15. lemma OAI.SharpTerminalLeave.PathForest.onPath_before line 78
  16. theorem OAI.SharpTerminalLeave.PathForest.parent_determined line 84
  17. inductive OAI.SharpTerminalLeave.PathForest.PathColor line 120
  18. instance OAI.SharpTerminalLeave.PathForest.(instance at line 124) line 124
  19. def OAI.SharpTerminalLeave.PathForest.color line 128
  20. lemma OAI.SharpTerminalLeave.PathForest.color_left_iff line 132
  21. lemma OAI.SharpTerminalLeave.PathForest.color_right_iff line 138
  22. theorem OAI.SharpTerminalLeave.PathForest.two_path_forest_count line 147