OAI/Combinatorics/Ramsey/CycleClique/ChainProfiles.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.CycleClique.ChainAmounts line 12
  2. theorem OAI.CycleClique.first_mem_split line 19
  3. theorem OAI.CycleClique.ChainAmounts.exists line 41
  4. theorem OAI.CycleClique.ChainAmounts.head_mem line 73
  5. theorem OAI.CycleClique.ChainAmounts.count line 77
  6. theorem OAI.CycleClique.ChainAmounts.deletion_split line 102
  7. def OAI.CycleClique.AmountProfile line 130
  8. theorem OAI.CycleClique.PathSystem.exists_profile line 134
  9. theorem OAI.CycleClique.AmountProfile.count line 151
  10. theorem OAI.CycleClique.AmountProfile.perm line 178
  11. theorem OAI.CycleClique.ChainAmounts.ends line 184
  12. theorem OAI.CycleClique.forallâ‚‚_select_right line 195
  13. theorem OAI.CycleClique.AmountProfile.delete line 208
  14. theorem OAI.CycleClique.AmountProfile.erase line 271
  15. theorem OAI.CycleClique.AmountProfile.drop_prefix line 278
  16. theorem OAI.CycleClique.AmountProfile.prune line 288
  17. theorem OAI.CycleClique.PathSystem.incident_le_twice_edgeCount line 294
  18. theorem OAI.CycleClique.ChainAmounts.run_bound line 333
  19. theorem OAI.CycleClique.AmountProfile.run_bound line 361
  20. theorem OAI.CycleClique.list_minimal_above line 371
  21. theorem OAI.CycleClique.list_sum_erase line 384
  22. theorem OAI.CycleClique.list_sum_lower line 388
  23. theorem OAI.CycleClique.increment_numeric line 393
  24. theorem OAI.CycleClique.PathSystem.small_increment line 400
  25. theorem OAI.CycleClique.PathSystem.join_tails_exact line 475