map_prod_eq_map₂ — Mathlib

English

The map of the product is equal to map₂ with uncurry: map (fst, snd) (f × g) = map₂ Prod.mk f g.

Русский

Образ отображения произведения равняется map₂ с раскрученной парой: map (fst, snd) (f × g) = map₂ Prod.mk f g.

LaTeX

$$$\\mathrm{map}\\; (\\lambda p. (p.fst, p.snd))\\ (f \\times\\! g) = \\mathrm{map\_2}\\; Prod.mk\\; f\\; g$$$

Lean4

theorem map_prod_eq_map₂ (m : α → β → γ) (f : Filter α) (g : Filter β) :
    Filter.map (fun p : α × β => m p.1 p.2) (f ×ˢ g) = map₂ m f g := by rw [map₂, copy_eq, uncurry_def]

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