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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble a Ramsey upper bound once the expanded counterexamples in its fixed cycle-length parameter have been excluded.

  1. theorem OAI.CycleClique.Construction.ramseyProperty_of_expanded_exclusion line 10
  2. theorem OAI.CycleClique.Construction.isRamseyNumber_of_expanded_exclusion line 24