Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 11:48 c5e13bd0

View on Github →

chore(combinatorics/set_family/intersecting): extract a repeated proof into a lemma (#17371)

Estimated changes

Modified src/combinatorics/set_family/intersecting.lean

modified theorem set.intersecting.card_le

added theorem set.intersecting.disjoint_map_compl