OAI/Combinatorics/Ramsey/CycleClique/ThreeCycles.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CycleClique.ThreeHyp line 28
  2. theorem OAI.CycleClique.ThreeHyp.separated line 40
  3. theorem OAI.CycleClique.ThreeHyp.U_nonempty line 50
  4. theorem OAI.CycleClique.ThreeHyp.alpha_sum line 54
  5. theorem OAI.CycleClique.ThreeHyp.a_eq line 62
  6. theorem OAI.CycleClique.ThreeHyp.U_clique line 71
  7. theorem OAI.CycleClique.ThreeHyp.U_card line 81
  8. def OAI.CycleClique.ThreeHyp.W line 87
  9. theorem OAI.CycleClique.ThreeHyp.W_outside line 90
  10. theorem OAI.CycleClique.ThreeHyp.W_not_U line 93
  11. theorem OAI.CycleClique.ThreeHyp.W_nonadj_Q line 97
  12. theorem OAI.CycleClique.ThreeHyp.W_card line 100
  13. theorem OAI.CycleClique.ThreeHyp.W_nonempty line 118
  14. theorem OAI.CycleClique.ThreeHyp.W_at_most_one line 126
  15. theorem OAI.CycleClique.ThreeHyp.indep_four_bound line 139
  16. theorem OAI.CycleClique.ThreeHyp.W_no_two_misses line 159
  17. theorem OAI.CycleClique.ThreeHyp.W_two_complete line 177
  18. theorem OAI.CycleClique.ThreeHyp.W_complete_singleton line 191
  19. theorem OAI.CycleClique.ThreeHyp.W_at_least_three line 201
  20. theorem OAI.CycleClique.ThreeHyp.no_two_common line 224
  21. theorem OAI.CycleClique.ThreeHyp.contradiction line 234