TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Erdős-Ko-Rado theorem: for $1\le k$ and $n\ge 2k$ , an intersecting family of $k$ -subsets of an $n$ -set has size at most $\binom{n-1}{k-1}$ , and a star attains the bound

Statement

Let $A$ be an $n$ -element set, where $1\le k$ and $n\ge2k$ . If $\mathcal F\subseteq[A]^k$ is intersecting, then

$|\mathcal F|\le\binom{n-1}{k-1}.$

For every fixed $a\in A$ , the star $\{S\in[A]^k:a\in S\}$ is intersecting and has cardinality $\binom{n-1}{k-1}$ , so the bound is attained. No uniqueness of extremal families is asserted.

Facts & Assumptions

Given: An $n$ -element set $A$ , natural numbers $1\le k$ and $n\ge2k$ , and an intersecting family $\mathcal F\subseteq[A]^k$ .

[L1]

In any cyclic order of $A$ , at most $k$ length- $k$ cyclic intervals can belong to a pairwise intersecting family (At most $k$ cyclic intervals of length $k$ in a cyclic order are pairwise intersecting when the ground-set size is at least $2k$ ).

[F1]

A $k$ -uniform family is intersecting when every two members meet, and a star consists of the $k$ -sets through one fixed point (Intersecting uniform families of finite sets, The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ ).

[L2]

An $m$ -element set has $m!$ orderings, and independent finite choices multiply (A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality, The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ , The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ ).

[L3]

The binomial closed formula gives $(n-1)!=(k-1)!(n-k)!\binom{n-1}{k-1}$ ( $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$ ; hence $\binom{n}{k}\,k! = n^{\underline{k}}$ , the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$ ).

Proof

technique · direct

1.1

A cyclic order of $A$ is a linear ordering modulo cyclic rotation. There are $(n-1)!$ cyclic orders: fix one element in the first position and order the remaining $n-1$ elements.

givenL2

1.2

Fix $S\in[A]^k$ . Exactly $k!(n-k)!$ cyclic orders make $S$ a cyclic interval: arrange the elements of $S$ within one consecutive block and arrange the elements of $A\setminus S$ in the complementary block.

givenL2

1.3

For a fixed $a\in A$ , deleting $a$ is a bijection from the star centred at $a$ to the $(k-1)$ -subsets of $A\setminus\{a\}$ . The star is intersecting because all its members contain $a$ , and its size is $\binom{n-1}{k-1}$ .

2.1

Count pairs $(\omega,S)$ where $\omega$ is a cyclic order and $S\in\mathcal F$ is a length- $k$ interval in $\omega$ . By step 1.2 there are $|\mathcal F|k!(n-k)!$ pairs.

step 1.2L2

3.1

By [L1], each of the $(n-1)!$ cyclic orders occurs in at most $k$ pairs. Hence $|\mathcal F|k!(n-k)!\le k(n-1)!$ .

step 1.1step 2.1L1

4.1

Cancelling the positive factor $k!(n-k)!=k(k-1)!(n-k)!$ in step 3.1 and using [L3] gives $|\mathcal F|\le\binom{n-1}{k-1}$ .

step 3.1L3algebra

5.1

Step 4.1 proves the upper bound and step 1.3 exhibits an intersecting family attaining it.

step 4.1step 1.3∎

Remarks

The hypothesis $n\ge2k$ is essential. At the boundary $n=2k$ , choosing exactly one set from each complementary pair already gives many extremal families, so the theorem deliberately does not claim that stars are the only extremizers.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 66 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Matoušek and J. Vondrák, The Probabilistic Method, pp. 14-15 (standard reference, not scraped)

Erdős-Ko-Rado theorem: for 1≤k1\le k1≤k and n≥2kn\ge 2kn≥2k, an intersecting family of kkk-subsets of an nnn-set has size at most (n−1k−1)\binom{n-1}{k-1}(k−1n−1​), and a star attains the bound