OAI/Combinatorics/Ramsey/CycleClique/CycleShortening.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.cycleGraph_adj_succ line 11
  2. theorem OAI.CycleClique.contains_cycle_of_labels line 17
  3. theorem OAI.CycleClique.fin_add_one_val line 26
  4. def OAI.CycleClique.bypassIndex line 34
  5. theorem OAI.CycleClique.bypassIndex_injective line 37
  6. theorem OAI.CycleClique.bypassIndex_step line 45
  7. def OAI.CycleClique.fourStepIndex line 64
  8. theorem OAI.CycleClique.fourStepIndex_injective line 69
  9. theorem OAI.CycleClique.fourStepIndex_step line 77
  10. theorem OAI.CycleClique.fin_ne_add_step line 96
  11. theorem OAI.CycleClique.shorten_cycle line 107
  12. theorem OAI.CycleClique.cycle_of_alpha_two_long_cycle line 157
  13. theorem OAI.CycleClique.size_test line 169
  14. abbrev OAI.CycleClique.exteriorEdges line 195