Combinatorics · existing Mathlib declaration

Erdős–Ko–Rado Theorem

Choose many r-element subsets of an n-element ground set, requiring every two chosen subsets to share at least one element. When r is no more than half of n, Erdős–Ko–Rado gives the numerical ceiling binom(n−1,r−1) for the number of chosen subsets.

intersecting set families
uniform set families
extremal combinatorics
iterated shadows
Kruskal–Katona theorem

The theorem at a glance

Erdős–Ko–Rado at a glance

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

An ivory extremal-set-theory poster states the pairwise-intersecting uniform-family bound and traces complements, an iterated shadow, disjointness, Kruskal–Katona, and Pascal counting. — Complements and an iterated-shadow bound turn pairwise intersection into the cardinality obstruction behind Erdős–Ko–Rado.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

Selected after original-pixel inspection of the theorem schematic scientific; theorem-specific structure, legibility, margins, and public claim boundary passed. — Pairwise intersection plus uniform size r and r ≤ n/2 forces |𝒜| ≤ binom(n−1,r−1).

Complementary intuition

A mathematical landmark

Erdős–Ko–Rado is a foundational extremal set theorem. Mathlib derives its upper bound through complements, an iterated shadow, disjointness, and the Lovász form of Kruskal–Katona, giving the page a theorem-specific checked proof architecture.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem Finset.erdos_ko_rado {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finset (Fin n))).Intersecting) (h₂ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₃ : r ≤ n / 2) : #𝒜 ≤ (n - 1).choose (r - 1)

Selected evidence declaration text

theorem Finset.erdos_ko_rado {n : ℕ} {𝒜 : Finset (Finset (Fin n))} {r : ℕ} (h𝒜 : (𝒜 : Set (Finset (Fin n))).Intersecting) (h₂ : (𝒜 : Set (Finset (Fin n))).Sized r) (h₃ : r ≤ n / 2) : #𝒜 ≤ (n - 1).choose (r - 1)

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Claim boundary

No new theorem is claimed

This page indexes Mathlib’s finite-family theorem for 𝒜 : Finset (Finset (Fin n)). The family is pairwise intersecting, every member has exactly r elements, and the hypothesis is exactly r ≤ n / 2. The selected declaration proves only #𝒜 ≤ (n−1).choose (r−1); it does not construct a star family, prove a separate sharpness result, or classify equality cases.

ProofAtlas did not originate the Erdős–Ko–Rado theorem or Mathlib’s declaration.
The selected declaration is not a theorem about arbitrary infinite set families.
It does not assert that all members share one common element.
It does not formalize an extremal construction or classify equality cases.
The generated explanation and visuals are not proof evidence.

Provenance

Origin and evidence stay separate

Existing declaration: Finset.erdos_ko_rado in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.erdos-ko-rado-theorem.v001
Source handling: Verified upstream reference; no mirrored source package