Commit 2020-09-01 03:18 fc57cf49

View on Github →

feat(data/{finset,finsupp,multiset}): more assorted lemmas (#4006) Another grab bag of facts from the Witt vector branch. Coauthored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.union_subset_union

added theorem multiset.disjoint_to_finset

added theorem multiset.to_finset_subset

added theorem multiset.to_finset_union

Modified src/data/finset/fold.lean

added theorem finset.fold_sup_bot_singleton

added theorem finset.fold_union_empty_singleton

Modified src/data/finset/lattice.lean

added theorem finset.mem_sup

added theorem finset.sup_subset

Modified src/data/finsupp/basic.lean

added theorem finsupp.mem_to_multiset

Modified src/data/multiset/basic.lean

added theorem multiset.count_ne_zero