getElem_inits — Mathlib

English

For inits(l).get(n) with n < length(inits(l)), it holds that inits(l)[n] = l.take n.

Русский

Для get в inits(l) при n < length(inits(l)) выполняется inits(l)[n] = l.take n.

LaTeX

$$$(\\operatorname{inits}(l)).\\operatorname{get} n = l.\\operatorname{take} n$$$

Lean4

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

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