scanl_val — Mathlib

English

The underlying List of scanl equals the List.scanl of the underlying List of the original vector.

Русский

Подлежащее представление scanl равно List.scanl от исходного списка вектора.

LaTeX

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

Lean4

/-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl`
of the underlying `List` of the original `Vector`.
-/
@[simp]
theorem scanl_val : ∀ {v : Vector α n}, (scanl f b v).val = List.scanl f b v.val
  | _ => rfl

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