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