toList_getElem — Mathlib

English

The i-th element of the underlying list equals the i-th element of the vector, provided i is less than the length of the list.

Русский

i-й элемент базового списка равен i-му элементу вектора, если i-й элемент находится в пределах списка.

LaTeX

$$$(v.toList)[i] = v[i] \quad (i < v.toList.length)$$$

Lean4

theorem toList_getElem (v : Vector α n) (i : ℕ) {hi : i < v.toList.length} : v.toList[i] = v[i]'(by simp_all) :=
  rfl

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