feat(combinatorics/set_family/kleitman): Kleitman's bound (#14543)
feat(combinatorics/set_family/kleitman): Kleitman's bound (#14543)

The union of `k` intersecting families over a type of cardinality `n` has size at most `2ⁿ - 2ⁿ⁻ᵏ`. This is the main result in [Families of Non-disjoint subsets](https://reader.elsevier.com/reader/sd/pii/S0021980066800121).





leanprover-community/mathlib,leanprover-community/mathlib