getD_default_eq_getI — Mathlib

English

The defaulted access to a list at position n yields the same result as the corresponding non-default access.

Русский

Доступ по индексу к списку с заданным значением по умолчанию дает тот же результат, что и неиспользование значения по умолчанию.

LaTeX

$$$$ l.getD n default = l.getI n, \quad \text{for all } n. $$$$

Lean4

theorem getD_default_eq_getI {n : ℕ} : l.getD n default = l.getI n :=
  rfl

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