Product_of_Subset_with_Intersection_v4
Provedgroup-theoryintersectionproofwikisubset-product
Let G be a group and X, Y, Z subsets of G. Then X * (Y ∩ Z) ⊆ (X * Y) ∩ (X * Z).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Product_of_Subset_with_Intersection_v4 {G : Type _} [Group G] (X Y Z : Set G) : {a * b | (a : G) (b : G) (_ : a ∈ X) (_ : b ∈ Y ∩ Z)} ⊆ {a * b | (a : G) (b : G) (_ : a ∈ X) (_ : b ∈ Y)} ∩ {a * b | (a : G) (b : G) (_ : a ∈ X) (_ : b ∈ Z)} := by sorrySource