English
For vectors xs: αⁿ and ys: βⁿ and a function f: α → β → γ, the pairwise map map₂ f xs ys can be realized as the second component of a two-argument accumulation with a unit state: map₂ f xs ys = (mapAccumr₂ (λ x y _ ⇒ ((), f x y)) xs ys ()).snd.
Русский
Для векторов xs: αⁿ и ys: βⁿ и функции f: α → β → γ отображение по парам map₂ f xs ys можно выразить как вторую компоненту аккумуляции с состоянием единицы: map₂ f xs ys = (mapAccumr₂ (λ x y _ ⇒ ((), f x y)) xs ys ()).snd.
LaTeX
$$$$ \\operatorname{map}_2 f\\, xs\\, ys \;=\; \\operatorname{snd}\\Bigl( \\operatorname{mapAccumr_2}\\bigl( \\lambda x\\, y\\, \\_ : \\mathrm{Unit}, ((), f(x,y))\\bigr)\\; xs\\; ys\\; () \\Bigr) $$$$
Lean4
protected theorem map₂_eq_mapAccumr₂ {f : α → β → γ} :
map₂ f xs ys = (mapAccumr₂ (fun x y (_ : Unit) ↦ ((), f x y)) xs ys ()).snd := by
induction xs, ys using Vector.revInductionOn₂ <;> simp_all
