Set_with_Complement_forms_Partition
Provedproofwikiset-complementuniverse
Let ∅ ⊂ S ⊂ univ. Then S and its complement Sᶜ form a partition of the universal set: S ∩ Sᶜ = ∅ and S ∪ Sᶜ = univ.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_with_Complement_forms_Partition {α : Type _} (S : Set α) (hne : S.Nonempty) (hne' : Sᶜ.Nonempty) : S ∩ Sᶜ = ∅ ∧ S ∪ Sᶜ = Set.univ := by sorrySource