Intersecting families #
This file defines intersecting families and proves their basic properties.
Main declarations #
Set.Intersecting: Predicate for a set of elements in a generalized boolean algebra to be an intersecting family.
Set.Intersecting.card_le: An intersecting family can only take up to half the elements, because
aᶜcannot simultaneously be in it.
Set.Intersecting.is_max_iff_card_eq: Any maximal intersecting family takes up half the elements.
- [D. J. Kleitman, Families of non-disjoint subsets][kleitman1966]