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