instGetElemNatLt — Mathlib

English

There is a canonical element access operation for vectors: for a vector of length n, the i-th element is obtained by indexing into the underlying list, valid for i < n.

Русский

Существует каноническое обращение к элементу вектора: для вектора длины n i-й элемент определяется обращением к i-му элементу соответствующего списка, если i < n.

LaTeX

$$$v[i] = v_{toList}[i] \quad (i < n)$$$

Lean4

instance : GetElem (Vector α n) Nat α fun _ i => i < n where getElem := fun x i h => get x ⟨i, h⟩

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