Kleitman's bound on the size of intersecting families #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 #
finset.card_bUnion_le_of_intersecting: Kleitman's theorem.
References #
theorem
finset.card_bUnion_le_of_intersecting
{ι : Type u_1}
{α : Type u_2}
[fintype α]
[decidable_eq α]
[nonempty α]
(s : finset ι)
(f : ι → finset (finset α))
(hf : ∀ (i : ι), i ∈ s → ↑(f i).intersecting) :
(s.bUnion 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.