Symmetric_Difference_with_Self_is_Empty_Set
Provedempty-setproofwikisymmetric-difference
The symmetric difference of a set with itself is the empty set: S △ S = ∅
Preamble
import Mathlib.Order.SymmDiff import Mathlib.Data.Set.Basic
Formal statement
theorem Symmetric_Difference_with_Self_is_Empty_Set {α : Type _} (S : Set α) : symmDiff S S = ∅ := by sorrySource