theorem ErdosKoRado.erdos_ko_rado_theorem {n k : ℕ} (hn : 2 * k ≤ n) (F : Finset (Finset (Fin n))) (hF_int : (↑F).Intersecting) (hF_sized : Set.Sized k ↑F) : F.card ≤ (n - 1).choose (k - 1)

(Theorem 1.2.9, Erdős–Ko–Rado) For $n \ge 2k$, an intersecting family of $k$-subsets of $[n]$ has size at most $\binom{n-1}{k-1}$.