Power_Set_of_Group_under_Induced_Operation_is_Semigroup
Provedgroup-theorypower-setproofwikisemigroupssubset-products
The power set of a group under the induced subset product operation forms a semigroup: the product is associative.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Algebra.Group.Defs
Formal statement
theorem Power_Set_of_Group_under_Induced_Operation_is_Semigroup {G : Type _} [Group G] (A B C : Set G) (x : G) (h : x ∈ Set.image2 (fun a b => a * b) (Set.image2 (fun a b => a * b) A B) C) : x ∈ Set.image2 (fun a b => a * b) A (Set.image2 (fun a b => a * b) B C) := by sorrySource