map₂_curry — Mathlib

English

The map of the uncurry of m over the product filter equals map₂ m f g: (f ×ˢ g).map (uncurry m) = map₂ m f g.

Русский

Отображение у развёрнутого m над произведением фильтров даёт map₂ m f g: (f ×ˢ g).map (uncurry m) = map₂ m f g.

LaTeX

$$$ (f \times^s g).\map (unccurry m) = map_2 m f g $$$

Lean4

@[simp]
theorem map₂_curry (m : α × β → γ) (f : Filter α) (g : Filter β) : map₂ m.curry f g = (f ×ˢ g).map m :=
  (map_prod_eq_map₂' _ _ _).symm

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