English
The Erdős–Ko–Rado theorem: the maximum size of an intersecting family of r-sets from an n-element universe is at most (n-1 choose r-1). This bound is sharp.
Русский
Теорема Эрдоса–Ко–Радо: максимальный размер пересекающегося семейства r-наборов из вселенной размером n не превосходит C(n-1, r-1). Границa достигается.
LaTeX
$$$|\mathcal{A}| \le {n-1 \choose r-1}$ for an intersecting family of r-subsets of an n-element set$$
Lean4
/-- 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. -/
theorem erdos_ko_rado {𝒜 : 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) := by
-- Take care of the r=0 case first: it's not very interesting.
rcases Nat.eq_zero_or_pos r with b | h1r
· convert Nat.zero_le _
rw [Finset.card_eq_zero, eq_empty_iff_forall_notMem]
refine fun A HA ↦ h𝒜 HA HA ?_
rw [disjoint_self_iff_empty, ← Finset.card_eq_zero, ← b]
exact h₂ HA
refine
le_of_not_gt fun size ↦
?_
-- Consider 𝒜ᶜˢ = {sᶜ | s ∈ 𝒜}
-- Its iterated shadow (∂^[n-2k] 𝒜ᶜˢ) is disjoint from 𝒜 by intersecting-ness
have : Disjoint 𝒜 (∂ ^[n - 2 * r] 𝒜ᶜˢ) :=
disjoint_right.2 fun A hAbar hA ↦
by
simp only [mem_shadow_iterate_iff_exists_sdiff, mem_compls] at hAbar
obtain ⟨C, hC, hAC, _⟩ := hAbar
exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)
have : r ≤ n := h₃.trans (Nat.div_le_self n 2)
have : 1 ≤ n :=
‹1 ≤ r›.trans
‹r ≤ n›
-- We know the size of 𝒜ᶜˢ since it's the same size as 𝒜
have z : (n - 1).choose (n - r) < #𝒜ᶜˢ := by
rwa [card_compls, choose_symm_of_eq_add (tsub_add_tsub_cancel ‹r ≤ n› ‹1 ≤ r›).symm]
-- and everything in 𝒜ᶜˢ has size n-r.
have h𝒜bar : (𝒜ᶜˢ : Set (Finset (Fin n))).Sized (n - r) := by simpa using h₂.compls
have kk :=
kruskal_katona_lovasz_form (i := n - 2 * r) (by cutsat) ((tsub_le_tsub_iff_left ‹1 ≤ n›).2 h1r) tsub_le_self h𝒜bar
z.le
have : n - r - (n - 2 * r) = r := by omega
rw [this] at kk
have : n.choose r < #(𝒜 ∪ ∂ ^[n - 2 * r] 𝒜ᶜˢ) :=
by
rw [card_union_of_disjoint ‹_›]
convert lt_of_le_of_lt (add_le_add_left kk _) (add_lt_add_right size _) using 1
convert Nat.choose_succ_succ _ _ using 3
all_goals rwa [Nat.sub_one, Nat.succ_pred_eq_of_pos]
apply this.not_ge
convert Set.Sized.card_le _
· rw [Fintype.card_fin]
rw [coe_union, Set.sized_union]
refine ⟨‹_›, ?_⟩
convert h𝒜bar.shadow_iterate
cutsat
