Power_Set_with_Union_is_Commutative_Monoid
Provedexamples-of-monoidspower-setproofwikiset-union
The power set of S with set union forms a commutative monoid with the empty set as identity.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Power_Set_with_Union_is_Commutative_Monoid {α : Type _} (S : Set α) (A B : Set α) (hA : A ⊆ S) (hB : B ⊆ S) : A ∪ B = B ∪ A ∧ ∅ ∪ A = A := by sorrySource