A-B

Stream: Is there code for X?

[George Shakan]

How do I write A - B with A, B finsets of the reals? I know how to do the sumset

[Ruben Van de Velde]

Does \ work?

[Mauricio Collares]

Given the mention of "sumset", I think $A-B$ means $\{a - b : a \in A, b \in B\}$ here, but I am not sure.

[Yaël Dillies]

Wait a day! We're missing it and I was adding it.

[George Shakan]

@Yaël Dillies Ah, ok great..keep me updated!

[Moritz Doll]

is using A + (-B) that much more lengthy for proofs?

[George Shakan]

@Moritz Doll I also tried this but it is also not defined

[Kevin Buzzard]

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]

It's defined but you need import algebra.pointwise, open_locale pointwise and some decidability assumptions

[Yaël Dillies]

It's defined but you need import algebra.pointwise, open_locale pointwise and some decidability assumptions

[Yaël Dillies]

Have a look at branch#solymosi

[George Shakan]

@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]

It looks like (-B) is defined for sets but not for finsets!

[Bhavik Mehta]

@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)