Theorems · Theorem · combinatorics

Finset.erdos_ko_rado

• 1000+ list: Erdős–Ko–Rado theorem

∀ {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ},
  (↑𝒜).Intersecting → Set.Sized r ↑𝒜 → r ≤ n / 2 → 𝒜.card ≤ (n - 1).choose (r - 1)

The Erdős–Ko–Rado theorem. The maximum size of an intersecting family in α where all sets have size r is bounded by (card α - 1).choose (r - 1). This bound is sharp.

Defined in

Mathlib.Combinatorics.SetFamily.KruskalKatona

Cited by

0 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound