OAI/Combinatorics/Ramsey/CycleClique/SystemInsertion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.PathSystem.vertices_ncard line 13
2. theorem OAI.CycleClique.OutsidePath.to_list line 19
3. theorem OAI.CycleClique.positive_interior_chain line 49
4. theorem OAI.CycleClique.PathSystem.no_one_representatives line 66
5. theorem OAI.CycleClique.isChain_insert_step line 84
6. theorem OAI.CycleClique.PathSystem.insert_step line 99
7. theorem OAI.CycleClique.PathSystem.no_one_consecutive line 170
8. abbrev OAI.CycleClique.PathSystem.representatives line 188
9. theorem OAI.CycleClique.PathSystem.representatives_ncard line 191