Theorems · Theorem · combinatorics

Finset.card_biUnion_le_of_intersecting

∀ {ι : Type u_1} {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] [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. 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.

Defined in

Mathlib.Combinatorics.SetFamily.Kleitman

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEqNonempty