English
Repeat of the get relation for scanl in the inductive step; expresses the same recurrence as scanl_get.
Русский
Повторение соотношения get для scanl в индуктивном шаге; выражает ту же рекуррентность, что и scanl_get.
LaTeX
$$$\\forall {i : \\mathrm{Fin} n},\\; (\\mathrm{scanl}(f,b,v)).get(i.succ) = f((\\mathrm{scanl}(f,b,v)).get(i.castSucc) , v.get(i))$$$
Lean4
/-- For an index `i : Fin n`, the nth element of `scanl` of a
vector `v : Vector α n` at `i.succ`, is equal to the application
function `f : β → α → β` of the `castSucc i` element of
`scanl f b v` and `get v i`.
This lemma is the `get` version of `scanl_cons`.
-/
@[simp]
theorem scanl_get (i : Fin n) : (scanl f b v).get i.succ = f ((scanl f b v).get (Fin.castSucc i)) (v.get i) :=
by
rcases n with - | n
· exact i.elim0
induction n generalizing b with
| zero =>
have i0 : i = 0 := Fin.eq_zero _
simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]
| succ n hn =>
rw [← cons_head_tail v, scanl_cons, get_cons_succ]
refine Fin.cases ?_ ?_ i
· simp only [get_zero, scanl_head, Fin.castSucc_zero, head_cons]
· intro i'
simp only [hn, Fin.castSucc_fin_succ, get_cons_succ]
