Zulip Chat Archive
Stream: Is there code for X?
Topic: A-B
George Shakan (Mar 09 2022 at 17:09):
How do I write A - B with A, B finsets of the reals? I know how to do the sumset
Ruben Van de Velde (Mar 09 2022 at 17:13):
Does \ work?
Mauricio Collares (Mar 09 2022 at 17:22):
Given the mention of "sumset", I think means here, but I am not sure.
Yaël Dillies (Mar 09 2022 at 17:27):
Wait a day! We're missing it and I was adding it.
George Shakan (Mar 09 2022 at 17:41):
@Yaël Dillies Ah, ok great..keep me updated!
Moritz Doll (Mar 09 2022 at 17:59):
is using A + (-B)
that much more lengthy for proofs?
George Shakan (Mar 09 2022 at 18:14):
@Moritz Doll I also tried this but it is also not defined
Kevin Buzzard (Mar 09 2022 at 18:21):
I think people are in general edgy about global instances of things like +
and -
on set X
and finset X
because different people use them to mean different things in different contexts (e.g. addition could be union, or xor, and negation could be complement etc). You might find that this stuff is there but switched off by default.
Yaël Dillies (Mar 09 2022 at 18:22):
It's defined but you need import algebra.pointwise
, open_locale pointwise
and some decidability assumptions
Yaël Dillies (Mar 09 2022 at 18:22):
It's defined but you need import algebra.pointwise
, open_locale pointwise
and some decidability assumptions
Yaël Dillies (Mar 09 2022 at 18:22):
Have a look at branch#solymosi
George Shakan (Mar 09 2022 at 18:32):
@Yaël Dillies It seems to me that + is defined but - is not? I had done all those things you mentioned (except I did not make any decidability assumptions)
Bhavik Mehta (Mar 09 2022 at 18:47):
It looks like (-B)
is defined for sets but not for finsets!
Bhavik Mehta (Mar 09 2022 at 18:48):
@George Shakan if I remember correctly, your theorem was stated for reals so the decidability assumptions won't be needed, we can just say open_locale classical
as well (ie change open_locale pointwise
to open_locale classical pointwise
)
Last updated: Dec 20 2023 at 11:08 UTC