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):
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):
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
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: May 08 2021 at 09:11 UTC