English
For a vector of length 1, scanl yields a vector consisting of the starting value and the mapped value of the single element, followed by nil.
Русский
Для вектора длины 1 scanl даёт вектор, состоящий из начального значения, затем f(b,x) и nil.
LaTeX
$$$\\forall {f:\\alpha \\to \\mathrm{m}\\beta}\\;{b}:{\\beta}\\; (v:\\mathrm{Vector}\\ \\alpha\\ 1),\\; \\mathrm{scanl}(f,b,v) = \\mathrm{cons}(b,\\mathrm{cons}(f(b,v. head),\\mathrm{nil}))$$$
Lean4
/-- The recursive step of `scanl` splits a vector made up of a single element
`x ::ᵥ nil : Vector α 1` into a `Vector` of the provided starting value `b : β`
and the mapped `f b x : β` as the last value.
-/
@[simp]
theorem scanl_singleton (v : Vector α 1) : scanl f b v = b ::ᵥ f b v.head ::ᵥ nil :=
by
rw [← cons_head_tail v]
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]
