Equivalence_of_Definitions_of_Symmetric_Difference
Provedproofwikiset-differenceset-intersectionset-unionsymmetric-difference
Let S and T be sets. The symmetric difference (S \ T) ∪ (T \ S) equals (S ∪ T) \ (S ∩ T).
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Equivalence_of_Definitions_of_Symmetric_Difference {α : Type _} (S T : Set α) : (S \ T) ∪ (T \ S) = (S ∪ T) \ (S ∩ T) := by sorrySource