# 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.

## References #

- [D. J. Kleitman,
*Families of non-disjoint subsets*][kleitman1966]

theorem
Finset.card_biUnion_le_of_intersecting
{ι : Type u_1}
{α : Type u_2}
[Fintype α]
[DecidableEq α]
[Nonempty α]
(s : Finset ι)
(f : ι → Finset (Finset α))
(hf : ∀ (i : ι), i ∈ s → Set.Intersecting ↑(f i))
:

Finset.card (Finset.biUnion s f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - Finset.card s)

**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.