Symmetric_Difference_of_Equal_Sets
Provedempty-setproofwikiset-equalitysymmetric-difference
The symmetric difference of two equal sets is the empty set: S = T ↔ S △ T = ∅
Preamble
import Mathlib.Order.SymmDiff import Mathlib.Data.Set.Basic
Formal statement
theorem Symmetric_Difference_of_Equal_Sets {α : Type _} (S T : Set α) : S = T ↔ symmDiff S T = ∅ := by sorrySource