Hypergraph Ramsey Numbers

This file defines the r-uniform hypergraph Ramsey number R_r(n).

noncomputable def Combinatorics.hypergraphRamsey (r n : ℕ) : ℕ

The r-uniform hypergraph Ramsey number R_r(n). The smallest natural number m such that every 2-coloring of the r-subsets of a set of size m contains a monochromatic subset of size n.

Equations

• Combinatorics.hypergraphRamsey r n = sInf {m : ℕ | ∀ (c : Finset (Fin m) → Bool), ∃ (S : Finset (Fin m)), S.card = n ∧ ∃ (color : Bool), ∀ e ⊆ S, e.card = r → c e = color}

theorem Combinatorics.le_hypergraphRamsey (r n : ℕ) (hne : {m : ℕ | ∀ (c : Finset (Fin m) → Bool), ∃ (S : Finset (Fin m)), S.card = n ∧ ∃ (color : Bool), ∀ e ⊆ S, e.card = r → c e = color}.Nonempty) : n ≤ hypergraphRamsey r n

n ≤ hypergraphRamsey r n when the set is nonempty.

theorem Combinatorics.hypergraphRamsey_self (r : ℕ) : hypergraphRamsey r r = r

hypergraphRamsey r r = r for any r.