def SetSystems.initialSegment {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : ℕ) : Finset (Fin n)

The image under a permutation σ of $\{0, 1, \ldots, k-1\}$: the first k elements of $[n]$ in the order induced by σ.

theorem SetSystems.lym_inequality_general {α : Type u_1} [Fintype α] {F : Finset (Finset α)} (hF : IsAntichain (fun (x1 x2 : Finset α) => x1 ⊆ x2) ↑F) : ∑ A ∈ F, (↑((Fintype.card α).choose A.card))⁻¹ ≤ 1

(LYM inequality, general form) For any antichain $F$ of subsets of a finite type $\alpha$, $\sum_{A \in F} \binom{|\alpha|}{|A|}^{-1} \le 1$.

theorem SetSystems.lym_inequality (n : ℕ) (F : Finset (Finset (Fin n))) (hF : IsAntichain (fun (x1 x2 : Finset (Fin n)) => x1 ⊆ x2) ↑F) : ∑ A ∈ F, 1 / ↑(n.choose A.card) ≤ 1

(Theorem 1.2.3, LYM inequality) For an antichain $F \subseteq 2^{[n]}$, $\sum_{A \in F} 1/\binom{n}{|A|} \le 1$.

theorem SetSystems.sperner_theorem (n : ℕ) (F : Finset (Finset (Fin n))) (hF : IsAntichain (fun (x1 x2 : Finset (Fin n)) => x1 ⊆ x2) ↑F) : F.card ≤ n.choose (n / 2)

(Theorem 1.2.2, Sperner's Theorem) Every antichain of subsets of $[n]$ has size at most $\binom{n}{\lfloor n/2 \rfloor}$.