English
For i ≥ 0, if i+1 is within bounds of the scanl sequence, then the (i+1)-th element is obtained by applying f to the i-th element of the scanl and the i-th element of l.
Русский
Для i ≥ 0, если i+1 попадает в диапазон индексов последовательности scanl, то (i+1)-й элемент задаётся как f( (i)-й элемент scanl, i-й элемент l ).
LaTeX
$$$$\forall i:\mathbb{N},\ (i+1) < |\operatorname{scanl} f b l| \implies \\ (\operatorname{scanl} f b l)_{i+1} = f\big((\operatorname{scanl} f b l)_i\big)\big(l_i\big).$$$$
Lean4
theorem getElem?_succ_scanl {i : ℕ} :
(scanl f b l)[i + 1]? = (scanl f b l)[i]?.bind fun x => l[i]?.map fun y => f x y := by
induction l generalizing b i with
| nil => simp only [scanl, getElem?_nil, Option.map_none, Option.bind_fun_none, getElem?_cons_succ]
| cons hd tl hl =>
simp only [scanl_cons, singleton_append]
cases i
· simp
· simp only [hl, getElem?_cons_succ]
