getD_append_right — Mathlib

English

If l.length ≤ n, then getD of l ++ l' at n equals getD of l' at n - length(l).

Русский

Если длина l ≤ n, то getD от l ++ l' в позиции n равен getD от l' в позиции n - длина(l).

LaTeX

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

Lean4

theorem getD_append_right (l l' : List α) (d : α) (n : ℕ) (h : l.length ≤ n) :
    (l ++ l').getD n d = l'.getD (n - l.length) d := by grind

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