Corollary 4.8: The Boolean Algebra B_n has the Sperner Property

This file proves Corollary 4.8 from Chapter 4 of Stanley's Algebraic Combinatorics: the Boolean algebra B_n (subsets of an n-element set, ordered by inclusion) has the Sperner property.

The proof uses:

• Proposition 4.4 (orderMatchings_imp_sperner): order matchings imply the Sperner property.
• Lemma 4.5 (booleanPoset_hasOrderRaisingMatching): B_n has order-raising matchings.
• Complement duality: lowering matchings are obtained by conjugating raising matchings with the set complement involution.

Main results

• booleanPoset_hasOrderLoweringMatching: B_n has order-lowering matchings at levels above n/2.
• booleanPoset_hasOrderMatchings: B_n has order matchings with pivot n/2.
• boolean_sperner: B_n has the Sperner property.

def SpernerProperty.booleanComplement (n : ℕ) (s : BooleanPoset n) : BooleanPoset n

Complement of a subset in B_n: the set difference Fin n \ s.

theorem SpernerProperty.booleanComplement_card (n : ℕ) (s : BooleanPoset n) : Finset.card (booleanComplement n s) = n - Finset.card s

theorem SpernerProperty.booleanComplement_involutive (n : ℕ) : Function.Involutive (booleanComplement n)

theorem SpernerProperty.booleanComplement_antitone (n : ℕ) : Antitone (booleanComplement n)

theorem SpernerProperty.booleanComplement_grade (n : ℕ) (s : BooleanPoset n) : grade ℕ (booleanComplement n s) = n - grade ℕ s

theorem SpernerProperty.booleanPoset_hasOrderLoweringMatching (n i : ℕ) (hi : n + 1 ≤ 2 * i) (hin : i ≤ n) : HasOrderLoweringMatching i

B_n has an order-lowering matching at level i when n + 1 ≤ 2 * i and i ≤ n. This is obtained by conjugating the order-raising matching at level n - i with set complement.

theorem SpernerProperty.booleanPoset_hasOrderMatchings (n : ℕ) : HasOrderMatchings (n / 2)

B_n has order matchings with pivot ⌊n/2⌋.

theorem SpernerProperty.boolean_sperner (n : ℕ) : HasSpernerProperty

Corollary 4.8. The Boolean algebra B_n has the Sperner property.