Subset_of_Subset_Product
Provedproofwikisubset-products
If X is a subset of Y, then the subset product X * Z is a subset of Y * Z.
Preamble
import Mathlib.Data.Set.Basic import Mathlib.Algebra.Group.Defs
Formal statement
theorem Subset_of_Subset_Product {α : Type _} [Mul α] (X Y Z : Set α) (h : X ⊆ Y) : Set.image2 (· * ·) X Z ⊆ Set.image2 (· * ·) Y Z := by sorrySource