Kneser hypergraphs

DefinitionErdős's Kneser hypergraph problem#✓fully proved

The statement that for all natural numbers \(n, k, r, t\) with \(r \ge 1\), \(t \ge 1\) and \(n \ge kr + (t - 1)(k - 1)\), every coloring of the \(r\)-element subsets of \(\{0, \dots, n - 1\}\) with \(t\) colors has a color class containing \(k\) pairwise disjoint \(r\)-element subsets.

def kneserHypergraphColoring : Prop :=
  ∀ n k r t : ℕ, 1 ≤ r → 1 ≤ t → k * r + (t - 1) * (k - 1) ≤ n →
    ∀ c : Finset (Fin n) → Fin t, ∃ (i : Fin t) (E : Finset (Finset (Fin n))),
      E ⊆ (Finset.univ : Finset (Fin n)).powersetCard r ∧ E.card = k ∧ (∀ e ∈ E, c e = i) ∧
        (E : Set (Finset (Fin n))).PairwiseDisjoint id

Used by 1

Used byAlon–Frankl–Lovász theorem on Kneser hypergraphs

TheoremAlon–Frankl–Lovász theorem on Kneser hypergraphs#●ready to prove

For all natural numbers \(n, k, r, t\) with \(r \ge 1\), \(t \ge 1\) and \(n \ge kr + (t - 1)(k - 1)\), every coloring of the \(r\)-element subsets of \(\{0, \dots, n - 1\}\) with \(t\) colors has a color class containing \(k\) pairwise disjoint \(r\)-element subsets.

Alon, Frankl and Lovász proved this for all positive \(n, k, r, t\) (Theorem 1.1; the case \(k = 2\) is Lovász's proof of Kneser's conjecture), and the bound on \(n\) is sharp; erdosproblems.com/780 lists the problem as proved.

public theorem_wanted kneserHypergraphColoring_holds : kneserHypergraphColoring

Sources

• T. F. Bloom, Erdős Problems, Problem #780, https://www.erdosproblems.com/780 (status PROVED); resolution: N. Alon, P. Frankl and L. Lovász, The chromatic number of Kneser hypergraphs, Trans. Amer. Math. Soc. 298 (1986), 359-370, Theorem 1.1: for positive integers n, k, r, t with n ≥ kr + (t - 1)(k - 1), if the r-subsets of an n-element set are partitioned into t families then one family contains k pairwise disjoint r-sets (conjectured by Erdős in 1973; k = 2 is Kneser's conjecture, proved by Lovász), https://web.math.princeton.edu/~nalon/PDFS/Publications/The%20chromatic%20number%20of%20Kneser%20hypergraphs.pdf.

Uses 1

Statement usesErdős's Kneser hypergraph problem

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.