mathlib3

a6269fe6 - 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).