union of a finset of finsets

Stream: maths

[Kevin Buzzard]

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]

Or am I supposed to be using monads?

[Kenny Lau]

finset.sup?

[Kevin Buzzard]

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

[Kevin Buzzard]

I can't use library_search to look for a definition

[Chris Hughes]

There's also bind

[Kenny Lau]

that's the monad road

[Chris Hughes]

Not really, it's exactly the function he wants with a monaddy name.

[Kevin Buzzard]

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.