getElem_tails — Mathlib

English

If n is less than the length of tails(l), then the nth element of tails(l) equals l.drop n.

Русский

Если n < length(tails(l)), то (tails(l))[n] = l.drop n.

LaTeX

$$$(\\operatorname{tails}(l))[n] = l.\\operatorname{drop} n$$$

Lean4

@[simp]
theorem getElem_tails (l : List α) (n : Nat) (h : n < (tails l).length) : (tails l)[n] = l.drop n := by
  induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

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