map_uncurry_prod — Mathlib

English

Same as above: the uncurry curry correspondence yields the same relation between map₂ and map over product.

Русский

Аналогично: развёрнутая связь через uncurry и curry сохраняет связь между map₂ и map над произведением.

LaTeX

$$$ (f \timesˢ g).map (uncurry m) = map₂ m f g $$$

Lean4

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

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