prodMap_map_product — Mathlib

English

For any f,g, the image of s × t under Prod.map f g equals the product of the images: image (Prod.map f g) (s ×ˢ t) = (image f s) ×ˢ (image g t).

Русский

Для любых отображений f,g изображение (s × t) под действием Prod.map f g равно произведению изображений: image (Prod.map f g) (s ×ˢ t) = (image f s) ×ˢ (image g t).

LaTeX

$$$\mathrm{image}(\mathrm{Prod.map}\; f\; g)\bigl( s \timesˢ t \bigr) = (s \mathrm{image} f) \timesˢ (t \mathrm{image} g)$$$

Lean4

theorem prodMap_map_product {δ : Type*} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) :
    (s ×ˢ t).map (f.prodMap g) = s.map f ×ˢ t.map g := by simpa [← coe_inj] using Set.prodMap_image_prod f g s t

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