head_scanl — Mathlib

English

If the scanl sequence is nonempty, its head equals the initial value b.

Русский

Если последовательность scanl непуста, её голова равна начальному значению b.

LaTeX

$$$$\forall f,b,l:\ (\text{Ne}(\operatorname{scanl} f b l, \varnothing))\;\Rightarrow\; (\operatorname{scanl} f b l).head(h) = b.$$$$

Lean4

@[simp]
theorem head_scanl (h : scanl f b l ≠ []) : (scanl f b l).head h = b := by cases l <;> simp

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