Symmetric_Difference_with_Complement
Provedproofwikiset-complementsymmetric-differenceuniverse
The symmetric difference of a set with its complement is the universe: S △ Sᶜ = univ
Preamble
import Mathlib.Order.SymmDiff import Mathlib.Data.Set.Basic
Formal statement
theorem Symmetric_Difference_with_Complement {α : Type _} (S : Set α) : symmDiff S Sᶜ = Set.univ := by sorrySource