getElem?_scanr_of_lt — Mathlib

English

For every i with i < l.length + 1, the i-th element of scanr f b l exists and equals Some (foldr f b (l.drop i)).

Русский

Для каждого i с i < l.length + 1 элемент i-ой позиции scanr f b l существует и равен Some (foldr f b (l.drop i)).

LaTeX

$$$ \\forall {l : List \\alpha} {f : \\alpha \\rightarrow \\beta \\rightarrow \\beta} {b : \\beta} {i : \\mathbb{N}}, i < l.length + 1 \\Rightarrow (scanr f b l)[i]? = Some (foldr f b (l.drop i)).$$$

Lean4

theorem getElem?_scanr_of_lt {i : ℕ} (h : i < l.length + 1) : (scanr f b l)[i]? = some (foldr f b (l.drop i)) := by
  simpa [getElem?_scanr h]

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