getD_eq_getD_getElem? — Mathlib

English

For any list l and element d, getD equals the element at n if defined via getElem?; otherwise equals default.

Русский

Для списка l и элемента d getD равен элементу на позиции n через getElem?, иначе — по умолчанию.

LaTeX

$$$$ l.getD n d = l[n]?.getD d $$$$

Lean4

theorem getD_eq_getD_getElem? (n : ℕ) : l.getD n d = l[n]?.getD d := by
  cases Nat.lt_or_ge n l.length with
  | inl h => rw [getD_eq_getElem _ _ h, getElem?_eq_getElem h, Option.getD_some]
  | inr h => rw [getD_eq_default _ _ h, getElem?_eq_none_iff.mpr h, Option.getD_none]

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