getI_append — Mathlib

English

Appending a list to another does not affect early indices: if n is less than the length of l, then (l ++ l') .getI n equals l .getI n.

Русский

При добавлении списка к списку на ранних позициях индексы не изменяются: если n < длина l, то (l ++ l').getI n = l.getI n.

LaTeX

$$$$ n < l.length \Rightarrow (l ++ l').getI n = l.getI n. $$$$

Lean4

theorem getI_append (l l' : List α) (n : ℕ) (h : n < l.length) : (l ++ l').getI n = l.getI n :=
  getD_append _ _ _ _ h

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