Zulip Chat Archive

Stream: maths

Topic: finset.sUnion


view this post on Zulip Scott Morrison (Apr 12 2020 at 05:01):

I can't find any sign of finset.sUnion : finset (finset A) -> finset A. Am I missing something?

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:03):

bind

view this post on Zulip Chris Hughes (Apr 12 2020 at 05:06):

It might be join

view this post on Zulip Scott Morrison (Apr 12 2020 at 05:08):

Hmm... bind isn't quite what I want, it's

def bind (s : finset α) (t : α  finset β) : finset β

view this post on Zulip Scott Morrison (Apr 12 2020 at 05:09):

and I can't find any sign of finset.join.

view this post on Zulip Scott Morrison (Apr 12 2020 at 05:10):

but I guess s.bind id will do.

view this post on Zulip Scott Morrison (Apr 12 2020 at 05:10):

Shall I just add join defined as that?

view this post on Zulip Scott Morrison (Apr 12 2020 at 05:10):

or am I meant to set up a monad instance?

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:17):

#find doesn't give me anything

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:31):

I wouldn't mind calling this sUnion instead of join. We mostly use set theoretic terminology in finset

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:32):

I'm pretty sure I've used bind id for this in the past, without bothering with a definition


Last updated: May 11 2021 at 16:22 UTC