English
For any function f : α → β and any vector xs of type α of length n, the map of f over xs equals the second component of mapAccumr applied to xs with an initial accumulator Unit and output f x at each step. Formally, map f xs = (mapAccumr (fun x (_ : Unit) ⇒ ((), f x)) xs ()).snd.
Русский
Для любой функции f: α → β и вектора xs типа α длины n композиция map f xs равна второй компоненте аккумулятора при применении mapAccumr к xs с начальными значениями Unit и выходом f x на каждом шаге. Формально: map f xs = (mapAccumr (fun x (_ : Unit) ⇒ ((), f x)) xs ()).snd.
LaTeX
$$$\mathrm{map}\ f\ xs = (\mathrm{mapAccumr}\ (\lambda x\ (_\colon\mathrm{Unit})\Rightarrow ((), f\ x))\ xs\ ()) . \mathrm snd$$$
Lean4
protected theorem map_eq_mapAccumr {f : α → β} : map f xs = (mapAccumr (fun x (_ : Unit) ↦ ((), f x)) xs ()).snd := by
induction xs using Vector.revInductionOn <;> simp_all
