mathlib3 documentation

combinatorics.set_family.kleitman

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 #

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) :

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.