Subset_Product_is_Subset_of_Generator_v4
Provedgeneratorsgroup-theoryproofwikisubset-product
Let G be a group and X, Y subsets of G. Then for any a in X, b in Y, a*b is in the subgroup generated by X ∪ Y.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Subset_Product_is_Subset_of_Generator_v4 {G : Type _} [Group G] (X Y : Set G) (a : G) (b : G) (ha : a ∈ X) (hb : b ∈ Y) : a * b ∈ Subgroup.closure (X ∪ Y) := by sorrySource