basic): lemmas about `filter`, `cons`, and `disj_union` (#15385)

Commit

3 years ago

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

Author

eric-wieser

Parents

6b2ebac6

mathlib3 ecaa2891 - feat(data/finset/basic): lemmas about `filter`, `cons`, and `disj_union` (#15385)

mathlib3
ecaa2891 - feat(data/finset/basic): lemmas about `filter`, `cons`, and `disj_union` (#15385)