Commit 2022-07-15 15:49 ecaa2891

View on Github →

feat(data/finset/basic): lemmas about filter, cons, and disj_union (#15385) The lemma names and statements match the existing multiset versions.

Estimated changes

Modified src/data/finset/basic.lean

modified def finset.disj_union

added theorem finset.disj_union_comm

added theorem finset.disj_union_empty

added theorem finset.disj_union_singleton

added theorem finset.empty_disj_union

added theorem finset.filter_cons

added theorem finset.filter_cons_of_neg

added theorem finset.filter_cons_of_pos

added theorem finset.filter_disj_union

added theorem finset.singleton_disj_union