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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The n=3, m≥6 part of the formula, conditional on the same precise published Hamiltonicity input as the size test.

  1. theorem OAI.CycleClique.Construction.cycle_clique_three_upper line 12
  2. theorem OAI.CycleClique.Construction.cycle_clique_three_ge_six line 23