OAI/Combinatorics/Ramsey/CycleClique/LargeSystems.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CycleClique.PathSystem.chains_nodup line 22
  2. theorem OAI.CycleClique.PathSystem.incident_eq_edges_add_chains line 30
  3. theorem OAI.CycleClique.PathSystem.amount_pos_iff line 39
  4. theorem OAI.CycleClique.PathSystem.rep_of_chain line 54
  5. theorem OAI.CycleClique.PathSystem.rep_iff_in_chain line 59
  6. theorem OAI.CycleClique.ClosedChain.rep_mem_Q_iff_head line 75
  7. theorem OAI.CycleClique.PathSystem.interior_rep_next line 95
  8. theorem OAI.CycleClique.ClosedChain.reps_Q_count line 119
  9. theorem OAI.CycleClique.PathSystem.reps_Q_count line 138
  10. theorem OAI.CycleClique.PathSystem.interior_reps_length line 151
  11. theorem OAI.CycleClique.PathSystem.chains_disjoint line 161
  12. theorem OAI.CycleClique.markedReps_head line 172
  13. theorem OAI.CycleClique.PathSystem.reverse_other_rep line 178
  14. theorem OAI.CycleClique.list_two_ne line 216
  15. theorem OAI.CycleClique.PathSystem.extra_rep line 231
  16. theorem OAI.CycleClique.terminal_classification_numeric line 242
  17. theorem OAI.CycleClique.PathSystem.orient_vertices line 263
  18. theorem OAI.CycleClique.PathSystem.representatives_subset line 268
  19. structure OAI.CycleClique.LargeSystem line 273
  20. theorem OAI.CycleClique.LargeSystem.degree line 291
  21. theorem OAI.CycleClique.LargeSystem.vertices_le line 294
  22. theorem OAI.CycleClique.LargeSystem.orient line 300
  23. theorem OAI.CycleClique.LargeSystem.no_one line 304
  24. theorem OAI.CycleClique.LargeSystem.misses_reps line 309
  25. theorem OAI.CycleClique.LargeSystem.extra_degree line 317
  26. theorem OAI.CycleClique.LargeSystem.interior_degree line 342
  27. theorem OAI.CycleClique.LargeSystem.reverse_degree line 355
  28. theorem OAI.CycleClique.LargeSystem.two_chains_degree line 368
  29. theorem OAI.CycleClique.LargeSystem.first_nonclique line 372
  30. theorem OAI.CycleClique.LargeSystem.first_pair line 378
  31. theorem OAI.CycleClique.sum_independence_local line 387
  32. theorem OAI.CycleClique.packing_balls line 419
  33. abbrev OAI.CycleClique.PathSystem.missing line 430
  34. theorem OAI.CycleClique.PathSystem.missing_eq_flat line 433
  35. theorem OAI.CycleClique.PathSystem.missing_subset_reps line 447
  36. theorem OAI.CycleClique.PathSystem.missing_subset_Q line 452
  37. theorem OAI.CycleClique.PathSystem.missing_ncard line 457
  38. theorem OAI.CycleClique.PathSystem.incident_add_missing line 466
  39. theorem OAI.CycleClique.PathSystem.amount_pos_used line 473
  40. theorem OAI.CycleClique.PathSystem.singleton_extra_rep line 484
  41. theorem OAI.CycleClique.PathSystem.interior_representatives_ncard line 498
  42. theorem OAI.CycleClique.LargeSystem.two_large_first line 512
  43. theorem OAI.CycleClique.LargeSystem.short line 545
  44. theorem OAI.CycleClique.LargeSystem.short_information line 622
  45. theorem OAI.CycleClique.LargeSystem.short_heads line 636
  46. theorem OAI.CycleClique.LargeSystem.no_short_interior line 642
  47. theorem OAI.CycleClique.LargeSystem.no_short_step line 646
  48. theorem OAI.CycleClique.LargeSystem.parameter line 656
  49. theorem OAI.CycleClique.LargeSystem.at_least_two_chains line 713
  50. theorem OAI.CycleClique.LargeSystem.second_triple line 727
  51. theorem OAI.CycleClique.PathSystem.incident_representatives_ncard line 742
  52. theorem OAI.CycleClique.LargeSystem.exclude_two_missing line 755
  53. theorem OAI.CycleClique.LargeSystem.exclude_three line 812
  54. theorem OAI.CycleClique.LargeSystem.exclude_five line 854