toList_scanl — Mathlib

English

The toList of a scanl equals the List.scanl of the toList of the original vector.

Русский

toList от scanl равен List.scanl от toList исходного вектора.

LaTeX

$$$\\forall {f}\\;{b}\\;{v:\\mathrm{Vector}\\ \\alpha\\ n},\\; (\\mathrm{scanl}(f,b,v)).\\mathrm{toList} = \\mathrm{List.scanl}(f,b,v.\\mathrm{toList})$$$

Lean4

/-- The `toList` of a `Vector` after a `scanl` is the `List.scanl`
of the `toList` of the original `Vector`.
-/
@[simp]
theorem toList_scanl : (scanl f b v).toList = List.scanl f b v.toList :=
  rfl

Похожие утверждения