drop_scanr — Mathlib

English

For i ≤ length(l), drop i (scanr f b l) = scanr f b (drop i l).

Русский

Для i ≤ длина(l) верно: drop i (scanr f b l) = scanr f b (drop i l).

LaTeX

$$$$\forall i:\mathbb{N},\ (i \le \operatorname{length}(l)) \Rightarrow \operatorname{drop} i (\operatorname{scanr} f b l) = \operatorname{scanr} f b (\operatorname{drop} i l).$$$$

Lean4

theorem drop_scanr {i : ℕ} (h : i ≤ l.length) : (scanr f b l).drop i = scanr f b (l.drop i) := by
  induction i with
  | zero => simp
  | succ i ih =>
    rw [← drop_drop]
    simp [ih (by cutsat), tail_scanr (l := l.drop i) (by rw [length_drop]; cutsat)]

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