Commit 2023-02-02 09:43 5d1947ab

View on Github →

Feat: Port Combinatorics.SetFamily.Intersecting (#2005) Mostly renaming. Re-write a proof where I can't make the old one work.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SetFamily/Intersecting.lean

added theorem Set.Intersecting.card_le

added theorem Set.Intersecting.disjoint_map_compl

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