English
Given two vectors v1 and v2 of the same length n and a binary function f, the i-th element of map₂ f v1 v2 is f(v1[i], v2[i]).
Русский
Пусть v1 и v2 — вектора длины n, и имеется бинарная функция f. Тогда i-й элемент map₂ f v1 v2 равен f(v1[i], v2[i]).
LaTeX
$$$\\mathrm{get}(\\mathrm{map₂} f\, v_1\, v_2)\\ i = f(\\mathrm{get}(v_1,i), \\mathrm{get}(v_2,i))$$$
Lean4
@[simp]
theorem get_map₂ (v₁ : Vector α n) (v₂ : Vector β n) (f : α → β → γ) (i : Fin n) :
get (map₂ f v₁ v₂) i = f (get v₁ i) (get v₂ i) :=
by
clear * - v₁ v₂
induction v₁, v₂ using inductionOn₂ with
| nil => exact Fin.elim0 i
| cons ih =>
rw [map₂_cons]
cases i using Fin.cases
· simp only [get_zero, head_cons]
· simp only [get_cons_succ, ih]
