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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The unconditional main formula for cycle lengths four and five.

  1. theorem OAI.CycleClique.Construction.cycle_clique_four_upper line 10
  2. theorem OAI.CycleClique.Construction.cycle_clique_five_upper line 16
  3. theorem OAI.CycleClique.Construction.cycle_clique_four line 22
  4. theorem OAI.CycleClique.Construction.cycle_clique_five line 29