English
Sperner's theorem: The size of an antichain in Finset α is at most the size of the largest level, i.e., #𝒜 ≤ C(n, ⌊n/2⌋) where n = |α|.
Русский
Теорема Sperner: Размер антицепи в Finset α не превосходит размер наибольшего слоя, то есть #𝒜 ≤ C(n, ⌊n/2⌋) при n = |α|.
LaTeX
$$$$ |𝒜| \\le \\binom{n}{\\lfloor n/2 \\rfloor}, \\quad n = |\\alpha|, \\ 𝒜 \\text{ антикольность} $$$$
Lean4
/-- **Sperner's theorem**. The size of an antichain in `Finset α` is bounded by the size of the
maximal layer in `Finset α`. This precisely means that `Finset α` is a Sperner order. -/
theorem _root_.IsAntichain.sperner (h𝒜 : IsAntichain (· ⊆ ·) 𝒜.toSet) :
#𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2) :=
by
have : 0 < ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0) := Nat.cast_pos.2 <| choose_pos (Nat.div_le_self _ _)
have h :=
calc
∑ s ∈ 𝒜, ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0)⁻¹
_ ≤ ∑ s ∈ 𝒜, ((Fintype.card α).choose #s : ℚ≥0)⁻¹ :=
by
gcongr with s hs
· exact mod_cast choose_pos s.card_le_univ
· exact choose_le_middle _ _
_ ≤ 1 := lubell_yamamoto_meshalkin_inequality_sum_inv_choose h𝒜
simpa [mul_inv_le_iff₀' this] using h
