ofList_get? — Mathlib

English

The mapping that turns a finite list into a sequence preserves index lookups: the nth element of the resulting sequence equals the nth element of the list, if defined.

Русский

Отображение, переводящее конечный список в последовательность, сохраняет поиск по индексу: n-й элемент полученной последовательности равен n-му элементу списка, если он существует.

LaTeX

$$$ \forall l:\mathrm{List}(\alpha), \forall n:\mathbb{N},\ (\mathrm{ofList\ }l).get?\ n = l[n]?.$$$

Lean4

@[simp]
theorem ofList_get? (l : List α) (n : ℕ) : (ofList l).get? n = l[n]? :=
  rfl

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