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