Complement_of_Empty_Set_is_Universe
Provedempty-setproofwikiset-complementuniverse
The complement of the empty set is the universe: ∅ᶜ = univ
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Complement_of_Empty_Set_is_Universe {α : Type _} : (∅ : Set α)ᶜ = Set.univ := by sorrySource