mathlib
ccf8aa04 - feat(data/finset/basic): disj_Union (#16421)

Commit
3 years ago
feat(data/finset/basic): disj_Union (#16421) `finset.disj_Union` is to `finset.bUnion` as: * `finset.disj_union` is to `finset.union` * `finset.cons` is to `insert` * `finset.map` is to `finset.image` Co-authored-by: Yaƫl Dillies <yael.dillies@gmail.com>
Author
Parents
Loading