getD_eq_getElem — Mathlib

English

For a list l and index n, the value obtained by getD at n equals the value obtained by indexing l if n is within bounds, otherwise the default value.

Русский

Для списка l и индекса n значение getD(l,n) совпадает с элементом списка l на позиции n, если n в пределах длины, иначе — с дефолтным значением.

LaTeX

$$$$\\forall l:\\, \\text{List }\\alpha,\\; \\forall d:\\, \\alpha,\\; \\forall n:\\, \\mathbb{N},\\; l.getD\\ n\\ d = \\begin{cases} l[n], & n < l.length \\\\ d, & \\text{иначе} \\end{cases} $$$$

Lean4

theorem getD_eq_getElem {n : ℕ} (hn : n < l.length) : l.getD n d = l[n] := by grind

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