OAI/Combinatorics/Ramsey/CycleClique/MarkedChains.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.markedReps line 11
  2. theorem OAI.CycleClique.markedReps_sublist line 15
  3. theorem OAI.CycleClique.markedReps_length line 25
  4. def OAI.CycleClique.MarkedCut line 43
  5. theorem OAI.CycleClique.markedCut_cons line 46
  6. theorem OAI.CycleClique.mem_markedReps line 52
  7. def OAI.CycleClique.PathSystem.reps line 78
  8. theorem OAI.CycleClique.markedReps_flatten_sublist line 81
  9. theorem OAI.CycleClique.PathSystem.reps_sublist line 89
  10. theorem OAI.CycleClique.markedReps_flatten_length line 93
  11. theorem OAI.CycleClique.PathSystem.reps_length line 105
  12. theorem OAI.CycleClique.markedCut_of_split line 110
  13. theorem OAI.CycleClique.two_mem_ordered line 120
  14. theorem OAI.CycleClique.markedCuts_ordered line 132
  15. def OAI.CycleClique.prefixChains line 143
  16. theorem OAI.CycleClique.prefixChains_flatten line 146
  17. theorem OAI.CycleClique.mem_prefixChains line 150
  18. theorem OAI.CycleClique.prefixChains_length_le line 154
  19. theorem OAI.CycleClique.prefix_ends line 158
  20. structure OAI.CycleClique.ClosedChain line 168
  21. structure OAI.CycleClique.LooseTail line 174
  22. theorem OAI.CycleClique.PathSystem.closed_chain line 179
  23. theorem OAI.CycleClique.ClosedChain.cut line 183
  24. theorem OAI.CycleClique.perm_reorder_four line 196
  25. theorem OAI.CycleClique.PathSystem.join_distinct_chains line 202
  26. theorem OAI.CycleClique.PathSystem.join_same_chain line 233
  27. theorem OAI.CycleClique.PathSystem.representative_replacement line 269
  28. abbrev OAI.CycleClique.PathSystem.vertices line 312