getElem_def — Mathlib

English

For a vector v of length n and an index i with hi: i < n, the i-th component of v is exactly the i-th component of its underlying list.

Русский

Для вектора v длинны n и индекса i с hi: i < n, i-й компонент вектора равен i-му компоненту его базового списка.

LaTeX

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

Lean4

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

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