Commit 2021-01-26 04:21 44fd23d1

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_.