mathlib

a5a6865f - feat(combinatorics/set_family/intersecting): Intersecting families (#14475)

feat(combinatorics/set_family/intersecting): Intersecting families (#14475) Define intersecting families, prove that intersecting families in `α` have size at most `card α / 2` and that all maximal intersecting families are this size.