Documentation

Mathlib.Combinatorics.SetFamily.Kleitman

Kleitman's bound on the size of intersecting families #

An intersecting family on n elements has size at most 2ⁿ⁻¹, so we could naïvely think that two intersecting families could cover all 2ⁿ sets. But actually that's not case because for example none of them can contain the empty set. Intersecting families are in some sense correlated. Kleitman's bound stipulates that k intersecting families cover at most 2ⁿ - 2ⁿ⁻ᵏ sets.

Main declarations #

References #

theorem Finset.card_biUnion_le_of_intersecting {ι : Type u_1} {α : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] (s : Finset ι) (f : ιFinset (Finset α)) (hf : is, (↑(f i)).Intersecting) :
(s.biUnion f).card 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)

Kleitman's theorem. An intersecting family on n elements contains at most 2ⁿ⁻¹ sets, and each further intersecting family takes at most half of the sets that are in no previous family.