getI_eq_iget_getElem? — Mathlib

English

For every n, the nth element of a list equals the value extracted from the nth optional index when present.

Русский

Для каждого n n-й элемент списка равен значению, извлечённому из n‑го опционального индекса, если он существует.

LaTeX

$$$$ l.getI n = (l[n]?.iget). $$$$

Lean4

theorem getI_eq_iget_getElem? (n : ℕ) : l.getI n = l[n]?.iget := by
  rw [← getD_default_eq_getI, getD_eq_getD_getElem?, Option.getD_default_eq_iget]

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