OAI/Combinatorics/Ramsey/CycleClique/PathSystems.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CycleClique.PathSystem line 9
  2. theorem OAI.CycleClique.clique_chains_flatten line 20
  3. theorem OAI.CycleClique.clique_chains_endpoints line 35
  4. theorem OAI.CycleClique.close_clique_chains line 50
  5. theorem OAI.CycleClique.flatten_singletons line 79
  6. def OAI.CycleClique.PathSystem.empty line 85
  7. def OAI.CycleClique.PathSystem.amount line 107
  8. def OAI.CycleClique.PathSystem.edgeCount line 111
  9. def OAI.CycleClique.PathSystem.singletons line 115
  10. def OAI.CycleClique.PathSystem.usedChains line 120
  11. def OAI.CycleClique.PathSystem.incident line 125
  12. theorem OAI.CycleClique.PathSystem.flat_length line 129
  13. theorem OAI.CycleClique.PathSystem.clique_count line 142
  14. theorem OAI.CycleClique.no_consecutive_count line 157
  15. theorem OAI.CycleClique.PathSystem.edgeCount_le_amount line 176
  16. theorem OAI.CycleClique.PathSystem.chains_length_le line 197
  17. theorem OAI.CycleClique.PathSystem.singletons_length_le line 213
  18. theorem OAI.CycleClique.PathSystem.partition line 218
  19. theorem OAI.CycleClique.singletons_flat_length line 225
  20. theorem OAI.CycleClique.PathSystem.singleton_flat_length line 234
  21. theorem OAI.CycleClique.PathSystem.closing_interval line 241
  22. theorem OAI.CycleClique.PathSystem.empty_amount line 280