Commit 2022-07-08 02:55 a5a6865f

View on Github →

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.

Estimated changes

Modified docs/references.bib

Created src/combinatorics/set_family/intersecting.lean

added theorem set.intersecting.card_le

added theorem set.intersecting.exists_card_eq

added theorem set.intersecting.exists_mem_finset

added theorem set.intersecting.exists_mem_set

added theorem set.intersecting.insert

added theorem set.intersecting.is_max_iff_card_eq

added theorem set.intersecting.is_upper_set'

added theorem set.intersecting.mono

added theorem set.intersecting.ne_bot

added theorem set.intersecting.not_bot_mem

added theorem set.intersecting.not_compl_mem

added theorem set.intersecting.not_mem

added def set.intersecting

added theorem set.intersecting_empty

added theorem set.intersecting_iff_eq_empty_of_subsingleton

added theorem set.intersecting_iff_pairwise_not_disjoint

added theorem set.intersecting_insert

added theorem set.intersecting_singleton

Modified src/order/upper_lower.lean

added theorem is_lower_set.bot_mem

added theorem is_lower_set.not_bot_mem

added theorem is_lower_set.top_mem

added theorem is_upper_set.bot_mem

added theorem is_upper_set.not_top_mem

added theorem is_upper_set.top_mem