English
Map a binary function over two vectors coordinatewise: map₂ f v w = zipWith f x y for the underlying lists.
Русский
Двоичную функцию применяют по координатам двух векторов: map₂ f v w = zipWith f x y на основаниях списков.
LaTeX
$$$\\forall f:\\alpha\\to\\beta\\to\\phi,\\forall v:\\text{Vector}(\\alpha,n),\\forall w:\\text{Vector}(\\beta,n),\\text{Vector }\\phi n = \\langle\\text{List.zipWith } f\\ (v{.}1)\\ (w{.}1),\\ \\text{proof}\\rangle$$$
Lean4
/-- Mapping two vectors under a curried function of two variables. -/
def map₂ (f : α → β → φ) : Vector α n → Vector β n → Vector φ n
| ⟨x, _⟩, ⟨y, _⟩ => ⟨List.zipWith f x y, by simp [*]⟩
