Inverse_of_Product_of_Subsets_of_Group
Provedgroup-theoryinverse-elementsproofwikisubset-products
In a group, (AB)⁻¹ = B⁻¹ * A⁻¹ for subset products.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Algebra.Group.Defs
Formal statement
theorem Inverse_of_Product_of_Subsets_of_Group {G : Type _} [Group G] (A B : Set G) (x : G) (h : x⁻¹ ∈ Set.image2 (fun a b => a * b) A B) : x ∈ Set.image2 (fun a b => a * b) (Set.image Inv.inv B) (Set.image Inv.inv A) := by sorrySource