Finset.card_biUnion_le_of_intersecting

theorem Finset.card_biUnion_le_of_intersecting : ∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : Nonempty α] (s : Finset ι) (f : ι → Finset (Finset α)), (∀ i ∈ s, (↑(f i)).Intersecting) → (s.biUnion f).card ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - s.card)

**Kleitman's theorem** states that for any type `ι` and `α`, where `α` is a finite type with a decidable equality and is nonempty, and `s` is a finite set of `ι` elements where each element maps to a set of sets of `α` elements that are intersecting, the cardinality of the set obtained by taking the binary union over `s` using the mapping function `f`, is less than or equal to `2` raised to the power of the cardinality of `α` minus `2` raised to the power of the difference between the cardinality of `α` and the cardinality of `s`. In simpler terms, the theorem asserts that an intersecting family on `n` elements contains at most `2^n - 1` sets, and each further intersecting family takes at most half of the sets that are not in any previous family.

More concisely: For any finite type `α` with decidable equality and a finite set `s` of functions from a type `ι` to sets of `α`, the number of intersecting sets in the binary union of `s` is at most 2^|α| - 2^(|α| - |s|), where |α| and |s| denote the cardinalities of `α` and `s` respectively.