OAI/Combinatorics/TriangleRemoval/Process/RestrictedParent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.PathForest.restrictedParent line 18
  2. def OAI.SharpTerminalLeave.PathForest.restrict line 26
  3. def OAI.SharpTerminalLeave.PathForest.index line 43
  4. lemma OAI.SharpTerminalLeave.PathForest.embed_index line 46
  5. lemma OAI.SharpTerminalLeave.PathForest.index_embed line 50
  6. lemma OAI.SharpTerminalLeave.PathForest.restrict_parent_some line 54
  7. lemma OAI.SharpTerminalLeave.PathForest.restrict_step_iff line 74
  8. lemma OAI.SharpTerminalLeave.PathForest.restrict_ancestor line 80
  9. lemma OAI.SharpTerminalLeave.PathForest.original_ancestor line 92
  10. def OAI.SharpTerminalLeave.PathForest.restrictMark line 101
  11. lemma OAI.SharpTerminalLeave.PathForest.restrict_onPath line 105
  12. theorem OAI.SharpTerminalLeave.PathForest.restrict_two_path_cover line 113