Set: symmetric difference

Stream: general

[Hunter Monroe]

I suggest defining the symmetric difference of two sets in data/set/basic.lean. Any reactions?

def set.symmetric_difference {α :Type*} (A B:set α) := (A \ B) ∪ (B \ A)
class has_symm_diff (α : Type*) := (symm_diff : α → α → α)

-- U+2206: symmetric difference
infixr ∆ :70 := has_symm_diff.symm_diff
instance set.has_symm_diff {α : Type*}: has_symm_diff (set α) := ⟨set.symmetric_difference⟩
lemma set.has_symm_diff.def {α : Type*} {A B:set α}:A ∆ B = (A \ B) ∪ (B \ A) := rfl

[Yakov Pechersky]

@Bryan Gin-ge Chen

[Yakov Pechersky]

I think Bryan had this in the works for a generalized boolean algebra, so that you get it for free on finset too

[Bryan Gin-ge Chen]

@Hunter Monroe I have a PR in progress at #6469. I can try to get back to it in a few days if you need this soon.

[Bryan Gin-ge Chen]

#6469 is now ready for review!