English
Let l be a finite list of elements of a type with a distinguished default element. Then, for every natural number n, if n is at least the length of l, the nth element obtained by safe indexing equals the default element.
Русский
Пусть l — конечный список элементов типа, у которого задан элемент по умолчанию. Тогда для любого натурального числа n, если n не меньше длины l, n-й элемент через безопасную индексацию равен значению по умолчанию.
LaTeX
$$$$ \forall l:\\mathrm{List}(\\alpha), \forall n:\\mathbb{N}, \ l.length \le n \Rightarrow l.getI n = \mathrm{default}. $$$$
Lean4
theorem getI_eq_default {n : ℕ} (hn : l.length ≤ n) : l.getI n = default :=
getD_eq_default _ _ hn
