OAI/Combinatorics/TriangleRemoval/Process/NonrootForest.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.TriangleGrowth.nonrootForest line 21
2. lemma OAI.SharpTerminalLeave.TriangleGrowth.nonrootForest_step line 28
3. lemma OAI.SharpTerminalLeave.TriangleGrowth.nonrootForest_ancestor line 34
4. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathNonroots_parent_closed line 41
5. lemma OAI.SharpTerminalLeave.TriangleGrowth.pathNonroots_cover line 51
6. def OAI.SharpTerminalLeave.TriangleGrowth.pathForest line 64
7. theorem OAI.SharpTerminalLeave.TriangleGrowth.pathForest_two_path_cover line 67
8. theorem OAI.SharpTerminalLeave.TriangleGrowth.older_focus line 73