getD_append — Mathlib

English

If n is less than the length of l, then getD of l ++ l' at n equals getD of l at n.

Русский

Если n меньше длины l, то getD от l ++ l' в позиции n равен getD от l в позиции n.

LaTeX

$$$$ n < |l| \\Rightarrow (l \\!\\!\\mathrm{append} \\ l').getD\\ n\\ d = l.getD\\ n\\ d $$$$

Lean4

theorem getD_append (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) : (l ++ l').getD n d = l.getD n d := by
  rw [getD_eq_getElem _ _ (Nat.lt_of_lt_of_le h (length_append ▸ Nat.le_add_right _ _)), getElem_append_left h,
    getD_eq_getElem]

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