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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The seven- and eight-cycle main clauses, with all finite obstructions excluded by finite certificates.

  1. theorem OAI.CycleClique.Construction.certificateCoverageAt_six line 11
  2. theorem OAI.CycleClique.Construction.certificateCoverageAt_seven line 19
  3. theorem OAI.CycleClique.Construction.cycle_clique_seven line 28
  4. theorem OAI.CycleClique.Construction.cycle_clique_eight line 32