English
For every vector v of length n and index i, the i-th element of v.get equals the corresponding element obtained from the underlying list, via the standard correspondence between Fin n and List indices.
Русский
Для каждого вектора v длины n и индекса i, i-й элемент v.get равен соответствующему элементу в списке во времени через стандартное соответствие между Fin n и индексами списка.
LaTeX
$$$\forall p\;\forall v:\mathrm{Vector}\,\alpha\,n\ (\forall x\in v.toList, p(x))\forall i\colon\mathbb{N}\; (hi:\ i< n)\; v.get\ i = v.toList.get (\mathrm{Fin.cast}\ (v.toList\_length).symm\ i)$$$
Lean4
theorem get_eq_get_toList (v : Vector α n) (i : Fin n) : v.get i = v.toList.get (Fin.cast v.toList_length.symm i) :=
rfl
