Union_with_Complement
Provedproofwikiset-complementset-unionuniverse
The union of a set and its complement is the universe: S ∪ Sᶜ = univ
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Union_with_Complement {α : Type _} (S : Set α) : S ∪ Sᶜ = Set.univ := by sorrySource