Zulip Chat Archive

Stream: maths

Topic: union of a finset of finsets


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:53):

Or am I supposed to be using monads?

view this post on Zulip Kenny Lau (Feb 18 2020 at 19:53):

finset.sup?

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:58):

I can't use library_search to look for a definition

view this post on Zulip Chris Hughes (Feb 18 2020 at 20:03):

There's also bind

view this post on Zulip Kenny Lau (Feb 18 2020 at 20:11):

that's the monad road

view this post on Zulip Chris Hughes (Feb 18 2020 at 20:12):

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

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 20:14):

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.


Last updated: May 10 2021 at 08:14 UTC