Subset_Product_within_Semigroup_is_Associative
Provedproofwikisubset-products
Let (S, *) be a semigroup. Then the subset product operation on the power set of S is also associative: (A * B) * C = A * (B * C).
Preamble
import Mathlib.Algebra.Group.Basic import Mathlib.Data.Set.Lattice
Formal statement
theorem Subset_Product_within_Semigroup_is_Associative {S : Type _} [Semigroup S] (A B C : Set S) : Set.image2 HMul.hMul (Set.image2 HMul.hMul A B) C = Set.image2 HMul.hMul A (Set.image2 HMul.hMul B C) := by sorrySource