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 #
Finset.card_biUnion_le_of_intersecting: Kleitman's theorem.
- [D. J. Kleitman, Families of non-disjoint subsets][kleitman1966]
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.