mathlib3
44fd23d1 - chore(data/finset): Rename bind to bUnion (#5813)

Commit
4 years ago
chore(data/finset): Rename bind to bUnion (#5813) This commit renames `finset.bind` to `finset.bUnion`. While this is the monadic bind operation, conceptually it's doing a bounded union of an indexed family of finite sets. This will help with discoverability of this function. There was a name conflict in `data.finset.lattice` due to this, since there are a number of theorems about the `set` version of `bUnion`, and for these I prefixed the lemmas with `set_`.
Author
Parents
Loading