Katona's union theorem

Proved

Katona.katona_union

by xbgxjack · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsextremal-set-theorykatonaunion-theorem

Katona's union theorem (even case). Let $F$ be a family of subsets of an $n$ -element ground set such that every two members $A, B \in F$ (allowing $A = B$ ) satisfy $|A \cup B| \le 2d$ . Then

|F| \le \sum_{i=0}^{d} \binom{n}{i},

the size of a Hamming ball of radius $d$ . This is the union-theorem counterpart of Katona's intersection theorem (Katona.katona): complementing every set in $F$ inside the $n$ -element ground set turns the union bound $|A \cup B| \le 2d$ into the intersection bound $|A^c \cap B^c| \ge n - 2d$ , so the complemented family is $(n-2d)$ -intersecting; applying the intersection theorem with $t = n - 2d$ and reindexing the resulting Hamming-ball bound (via $i \mapsto n - i$ and the symmetry $\binom{n}{i} = \binom{n}{n-i}$ ) yields exactly the claimed bound $\sum_{i=0}^d \binom{n}{i}$ .

Formalization note. The hypothesis 2 * d < n ensures $t := n - 2d$ satisfies $1 \le t \le n$ and $n + t$ is even, so Katona.katona applies directly to the complemented family.

Preamble

import Mathlib

Formal statement

namespace Katona

theorem katona_union {n d : ℕ} (hd : 2 * d < n) (F : Finset (Finset (Fin n)))
    (hF : ∀ A ∈ F, ∀ B ∈ F, (A ∪ B).card ≤ 2 * d) :
    F.card ≤ ∑ i ∈ Finset.range (d + 1), n.choose i := by sorry

end Katona

Source

G. O. H. Katona, Intersection theorems for systems of finite sets, Acta Math. Acad. Sci. Hungar. 15 (1964), 329-337 (union theorem derived by complementation from the intersection theorem).

View graph