## Stream: maths

### Topic: union of a finset of finsets

#### Kevin Buzzard (Feb 18 2020 at 19:52):

I want to take a finset's worth of union of finsets. Finsets are an instance of semilattice_sup_bot which seems to me to be precisely what one needs to make it possible to iterate ⊔ a finset number of times (⊔ is commutative and associative in a lattice). Is there a finset-indexed iterated ⊔ in Lean?

#### Kevin Buzzard (Feb 18 2020 at 19:53):

Or am I supposed to be using monads?

#### Kenny Lau (Feb 18 2020 at 19:53):

finset.sup?

#### Kevin Buzzard (Feb 18 2020 at 19:58):

Thanks. That's really annoying. I had all the ingredients but still failed to search (I looked before I asked)

#### Kevin Buzzard (Feb 18 2020 at 19:58):

I can't use library_search to look for a definition

#### Chris Hughes (Feb 18 2020 at 20:03):

There's also bind

#### Kenny Lau (Feb 18 2020 at 20:11):

I thought it might be. So because finset.sup works for all lattices but finset.bind only works for finsets of finsets, I should probably use bind  because there might be more lemmas.