Zulip Chat Archive

Stream: new members

Topic: Symmetric difference

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.?

Jeremy Avigad (May 31 2020 at 14:42):

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

Kevin Buzzard (May 31 2020 at 16:33):

Is there more than one way to do it constructively?

Kevin Buzzard (May 31 2020 at 16:34):

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

Kevin Buzzard (May 31 2020 at 16:35):

(as far as a constructivist is concerned)

Reid Barton (May 31 2020 at 16:40):

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

Bryan Gin-ge Chen (May 31 2020 at 16:47):

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

Kevin Buzzard (May 31 2020 at 17:46):

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

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.

Kevin Buzzard (May 31 2020 at 19:04):

Maybe we should introduce niff

Mario Carneiro (May 31 2020 at 20:23):

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

Mario Carneiro (May 31 2020 at 20:24):

If so then you can get sets using the pi instance

Last updated: Dec 20 2023 at 11:08 UTC