OAI/Combinatorics/Ramsey/CycleClique/ChainRearrangement.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.ChainAmounts.join line 14
  2. theorem OAI.CycleClique.ChainAmounts.reverse line 24
  3. theorem OAI.CycleClique.AmountProfile.of_reordered line 34
  4. theorem OAI.CycleClique.ChainAmounts.forallâ‚‚_exists line 41
  5. theorem OAI.CycleClique.AmountProfile.join_starts line 52
  6. theorem OAI.CycleClique.PathSystem.join_distinct_chains_exact line 74
  7. theorem OAI.CycleClique.PathSystem.join_same_chain_exact line 107
  8. theorem OAI.CycleClique.PathSystem.small_increment_run line 144
  9. theorem OAI.CycleClique.prefixChains_length_eq line 159
  10. theorem OAI.CycleClique.PathSystem.short_distinct_chains line 163
  11. theorem OAI.CycleClique.PathSystem.not_short_same_chain line 214
  12. theorem OAI.CycleClique.PathSystem.insert_step_run line 238
  13. theorem OAI.CycleClique.PathSystem.short_representatives line 310
  14. theorem OAI.CycleClique.PathSystem.not_short_consecutive line 366
  15. def OAI.CycleClique.flipChain line 381
  16. theorem OAI.CycleClique.flipChain_length line 384
  17. theorem OAI.CycleClique.flipChain_perm line 387
  18. theorem OAI.CycleClique.flipChains_flatten_perm line 390
  19. def OAI.CycleClique.PathSystem.orient line 396
  20. theorem OAI.CycleClique.PathSystem.orient_chains line 432
  21. theorem OAI.CycleClique.PathSystem.orient_perm line 436
  22. theorem OAI.CycleClique.PathSystem.orient_amount line 440
  23. theorem OAI.CycleClique.PathSystem.orient_edgeCount line 446
  24. theorem OAI.CycleClique.PathSystem.orient_singletons_length line 450
  25. theorem OAI.CycleClique.PathSystem.orient_incident line 459
  26. theorem OAI.CycleClique.PathSystem.orient_optimal line 463