OAI/Combinatorics/Ramsey/CycleClique/RamseyNumbers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Least forcing orders and the cycle–clique Ramsey number.

  1. def OAI.CycleClique.IsRamseyNumber line 10

    Source documentation

    The exact least order forcing a cycle or a complementary clique.

    def IsRamseyNumber (m n N : ℕ) : Prop :=
…
  2. theorem OAI.CycleClique.cycleCliqueRamsey_eq_of_isRamseyNumber line 13