English
There is a natural equivalence between length-n vectors over α and functions from Fin n to α, given by get and ofFn with inverse provided by get_ofFn and its inverse.
Русский
Существует естественное эквиваленство между векторами длины n над α и функциями Fin n → α, задаваемое get и ofFn, с обратной связностью через get_ofFn.
LaTeX
$$$\mathrm{Equiv}.\mathrm{vectorEquivFin} (\alpha)(n):\ Vector\alpha\ n \simeq (\mathrm{Fin}\ n \to \alpha)$, определено как $(\mathrm{get},\mathrm{ofFn},\mathrm{ofFn\_get},\ \text{инверсия})$$$
Lean4
/-- The natural equivalence between length-`n` vectors and functions from `Fin n`. -/
def _root_.Equiv.vectorEquivFin (α : Type*) (n : ℕ) : Vector α n ≃ (Fin n → α) :=
⟨Vector.get, Vector.ofFn, Vector.ofFn_get, fun f => funext <| Vector.get_ofFn f⟩
