## Stream: Is there code for X?

### Topic: symmetric difference / disjunctive union of sets

#### Eric Wieser (Feb 25 2021 at 17:26):

Do we have an operator for this, or am I expected to write it out in terms of intersection / union / difference?

#### Adam Topaz (Feb 25 2021 at 17:27):

disjoin union is \sum (on the type level), but that's the best you can do in general.

#### Adam Topaz (Feb 25 2021 at 17:28):

The usual notation for symmetric difference is something like $A \Delta B$, I think? I haven't seen that in lean.

#### Eric Wieser (Feb 25 2021 at 17:28):

Even a method of set would be fine for me

#### Adam Topaz (Feb 25 2021 at 17:30):

variables {α : Type*} (A B : set α)

def symmetric_difference := (A ∪ B) \ (A ∩ B)

notation A Δ B := symmetric_difference A B


#### Eric Wieser (Feb 25 2021 at 17:30):

Whoops, used the wrong word in the title - it's specifically symmetric difference I'm after

#### Adam Topaz (Feb 25 2021 at 17:31):

i don't know how strongly this notation should bind though....

#### Eric Wieser (Feb 25 2021 at 17:32):

Would it be appropriate to add set.symm_diff (without notation) to mathlib?

#### Gabriel Ebner (Feb 25 2021 at 17:32):

If we add such a notation, it should probably be a type class and also be defined for finset.

#### Adam Topaz (Feb 25 2021 at 17:32):

I don't see why not. It's a common enough construction.

#### Adam Topaz (Feb 25 2021 at 17:32):

Gabriel Ebner said:

If we add such a notation, it should probably be a type class and also be defined for finset.

Maybe even make it something in an arbitrary lattice?

#### Eric Wieser (Feb 25 2021 at 17:33):

Do we have sdiff on arbitrary lattices?

#### Bryan Gin-ge Chen (Feb 25 2021 at 17:34):

You can define it in terms of join and meet and complementation per https://en.wikipedia.org/wiki/Boolean_ring#Relation_to_Boolean_algebras

edit: Maybe symmetric difference only really makes sense on boolean algebras?

#### Adam Topaz (Feb 25 2021 at 17:34):

We have a docs#has_sdiff class which I've never seen used...

#### Adam Topaz (Feb 25 2021 at 17:34):

Oh docs#set.has_sdiff but this is just defined as set.diff!

#### Eric Wieser (Feb 25 2021 at 17:35):

You literally just used it!

#### Eric Wieser (Feb 25 2021 at 17:35):

But docs#boolean_algebra.to_has_sdiff is the answer to my question

#### Adam Topaz (Feb 25 2021 at 17:35):

What is sdiff?

#### Adam Topaz (Feb 25 2021 at 17:35):

s doesn't stand for symmetric?

#### Eric Wieser (Feb 25 2021 at 17:36):

I think s stands for "set"

#### Eric Wieser (Feb 25 2021 at 17:38):

Unicode seems to think that ⊖ is the appropriate symbol for symmetric difference

#### Adam Topaz (Feb 25 2021 at 17:41):

We probably don't want to rely on compl because then we won't get it for finsets.

#### Gabriel Ebner (Feb 25 2021 at 17:41):

When I search for "symmetric" in the unicode character picker, I get U+2206 ∆ (which is of course different from Δ, or 𝚫, or even 𝞓).

#### Adam Topaz (Feb 25 2021 at 17:43):

But if we only use sdiff and sup in the definition, that would be okay for finsets:

import order.lattice

def symmetric_difference {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

notation A Δ B := symmetric_difference A B


#### Eric Wieser (Feb 25 2021 at 17:54):

My comment was in reference to https://www.fileformat.info/info/unicode/char/2296/index.htm, which has "symmetric difference" in its index entries. Perhaps thats non-normative though.

#### Eric Wieser (Feb 25 2021 at 17:56):

2206 looks to be "increment", as in what I would normally read as "delta"

#### Mario Carneiro (Feb 25 2021 at 18:06):

heh, I think I would read them all as delta

unicode is nuts

#### Gabriel Ebner (Feb 25 2021 at 18:08):

2206 also has "symmetric difference (in set theory)" in the comments

#### Eric Wieser (Feb 25 2021 at 18:12):

I don't feel strongly about the notation - a global symm_diff function with associated typeclass would be fine by me too

#### Johan Commelin (Feb 25 2021 at 18:22):

I certainly think that whatever version of Delta is used, it should be localized notation. It's good to be reminded that the notation is being used.

#### Eric Wieser (Feb 25 2021 at 18:45):

Do we want to use sup or union, given that the s in sdiff is set?

#### Bryan Gin-ge Chen (Feb 25 2021 at 18:58):

sup would let this work for boolean algebras, right?

True

#### Kevin Buzzard (Feb 25 2021 at 20:57):

This is the addition which, together with multiplication = intersection, gives us the ring structure on set X related to filters I guess.

#### Bryan Gin-ge Chen (Feb 25 2021 at 21:12):

It's the addition in boolean rings. Boolean rings and Stone's representation theorem would be nice projects...

#### Bhavik Mehta (Feb 25 2021 at 23:28):

Adam Topaz said:

But if we only use sdiff and sup in the definition, that would be okay for finsets:

import order.lattice

def symmetric_difference {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

notation A Δ B := symmetric_difference A B


I used this notion as part of the proof in https://github.com/leanprover-community/mathlib/blob/e8c8ce914f4fbf23bfe25b4ae5083bdd8b6642fe/src/combinatorics/colex.lean#L164, and I'm pretty sure for a bunch of other things way back when I did kruskal-katona

#### Bryan Gin-ge Chen (Feb 27 2021 at 02:51):

I have some code now proving the equivalence between boolean algebras and boolean rings. The most annoying part, perhaps not surprisingly, was proving that the symmetric difference is associative. I'll try to break this up into PRs this weekend.

#### Bryan Gin-ge Chen (Feb 27 2021 at 19:15):

@Eric Wieser Do you have a branch in progress where you're using symmetric_difference? I'm thinking of adding it in a PR soon in the following form:

/-- The symmetric difference of a structure with ⊔ and \ is (A \ B) ⊔ (B \ A). -/
def symm_diff {α : Type*} [has_sup α] [has_sdiff α] (A B : α) := (A \ B) ⊔ (B \ A)

infix  Δ :100 := symm_diff


No, I don't

#### Eric Wieser (Feb 27 2021 at 19:49):

Feel free to add it though

#### Eric Wieser (Feb 27 2021 at 19:50):

(I have one line of a translation of some isabelle code that would use it, but that's it)

#### Bhavik Mehta (Feb 27 2021 at 19:55):

Eric Wieser said:

Do we have sdiff on arbitrary lattices?

Perhaps we should add a comment somewhere saying that sdiff means set difference, this certainly isn't the first time this confusion has happened

#### Bryan Gin-ge Chen (Feb 27 2021 at 19:56):

Good idea, I'll do that in one of my forthcoming PRs.

#### Bryan Gin-ge Chen (Feb 28 2021 at 08:22):

The PRs building up to the equivalence between Boolean algebras and Boolean rings are:

• #6460: "algebraic" constructors for (semi-)lattices
• #6464: Boolean rings (also has boolean_ring.to_boolean_algebra)
• #6469: symmetric difference operator
• #6476: boolean_algebra.to_boolean_ring

#6476 should probably have an equiv but I wasn't able to figure out how to prove equality between structures / classes. I'll start another thread about it.

Last updated: May 16 2021 at 05:21 UTC