Zulip Chat Archive

Stream: new members

Topic: Symmetric difference


view this post on Zulip Daniel Fabian (May 31 2020 at 14:40):

I want to use symmetric difference but can't seem to find it in either mathlib or standard libary. Am I just missing the name or should I define it myself.?

view this post on Zulip Jeremy Avigad (May 31 2020 at 14:42):

I don't think it is in the library...

view this post on Zulip Kevin Buzzard (May 31 2020 at 16:33):

Is there more than one way to do it constructively?

view this post on Zulip Kevin Buzzard (May 31 2020 at 16:34):

and and or are unambiguous inductive types, but maybe there are several xor on Prop?

view this post on Zulip Kevin Buzzard (May 31 2020 at 16:35):

(as far as a constructivist is concerned)

view this post on Zulip Reid Barton (May 31 2020 at 16:40):

Yes, probably. Where does symmetric difference actually come up?

view this post on Zulip Bryan Gin-ge Chen (May 31 2020 at 16:47):

It's addition in the Boolean ring structure on power sets.

view this post on Zulip Kevin Buzzard (May 31 2020 at 17:46):

Right. Is this constructively a Boolean ring? Maybe it's only a Propian ring...

view this post on Zulip Chris Hughes (May 31 2020 at 18:07):

I think not (a iff b) also works constructively. I don't think a iff not b is constructively associative or commutative.

view this post on Zulip Kevin Buzzard (May 31 2020 at 19:04):

Maybe we should introduce niff

view this post on Zulip Mario Carneiro (May 31 2020 at 20:23):

Do we have that Prop is a boolean ring? (which is equivalent to LEM)

view this post on Zulip Mario Carneiro (May 31 2020 at 20:24):

If so then you can get sets using the pi instance


Last updated: May 08 2021 at 09:11 UTC