prodMap_image_prod — Mathlib

English

The image of the product s × t under Prod.map f g equals the product of the images: (Prod.map f g) '' (s × t) = (f '' s) × (g '' t).

Русский

Образ произведения s × t под действием отображений Prod.map f g равен произведению образов: (Prod.map f g) '' (s × t) = (f '' s) × (g '' t).

LaTeX

$$$ (\operatorname{Prod.map} f g) '' (s \times t) = (f '' s) \times (g '' t) $$$

Lean4

theorem prodMap_image_prod (f : α → β) (g : γ → δ) (s : Set α) (t : Set γ) :
    (Prod.map f g) '' (s ×ˢ t) = (f '' s) ×ˢ (g '' t) := by
  ext
  aesop

Похожие утверждения