map_prod_eq_map₂' — Mathlib

English

Alternative expression: map_prod_eq_map₂' states equivalence with a curry-based version of map₂.

Русский

Альтернативная формулировка: map_prod_eq_map₂' эквивалентна по варианту карри map₂.

LaTeX

$$$\\mathrm{map\\_prod\\_eq\\_map\\_2'}(m,f,g)$$$

Lean4

theorem map_prod_eq_map₂' (m : α × β → γ) (f : Filter α) (g : Filter β) :
    Filter.map m (f ×ˢ g) = map₂ (fun a b => m (a, b)) f g :=
  map_prod_eq_map₂ m.curry f g

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