Commit 2022-11-05 13:58 7951ed37
View on Github →feat(data/finset/basic): add lemmas about filter and (co)disjoint (#17296)
This generalizes finset.filter_inter_filter_neg_eq to when the sets are different, and then further to when the propositions are not complementary but only disjoint.
A similar story is true of the union lemma.