English
The scanl of a vector built by prepending an element x to v equals the vector starting with b followed by scanl on v with f b x.
Русский
Сканирование вектора, образованного добавлением x спереди к v, равно вектору, начинающемуся с b и продолжающемуся как scanl f (f b x) v.
LaTeX
$$$\\forall a:\\alpha\\; (v:\\mathrm{Vector}\\ \\alpha\\ n),\\; \\mathrm{scanl}(f,b,\\mathrm{cons}(a,v)) = \\mathrm{cons}(b,\\mathrm{scanl}(f,(f\\,b\\,a),v))$$$
Lean4
/-- The recursive step of `scanl` splits a vector `x ::ᵥ v : Vector α (n + 1)`
into the provided starting value `b : β` and the recursed `scanl`
`f b x : β` as the starting value.
This lemma is the `cons` version of `scanl_get`.
-/
@[simp]
theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v :=
rfl
