OAI/Combinatorics/Ramsey/CycleClique/Construction/FourCycleClassCounts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The last three-class pigeonhole step in the four-cycle exclusion.

  1. theorem OAI.CycleClique.Construction.fin_three_two_of_not line 8
  2. theorem OAI.CycleClique.Construction.three_sizes_sum_le_four line 24
  3. theorem OAI.CycleClique.Construction.fourCycle_exterior_residual_total line 44