English
Vector3 α n is defined as the type Fin2 n → α, i.e., a vector of length n is a function on Fin2 n.
Русский
Vector3 α n задаётся как тип Fin2 n → α, то есть вектор длины n — функция на Fin2 n.
LaTeX
$$$\mathrm{Vector3}(\alpha,n) = \mathrm{Fin2}(n) \to \alpha$$$
Lean4
/-- Alternate definition of `Vector` based on `Fin2`. -/
def Vector3 (α : Type u) (n : ℕ) : Type u :=
Fin2 n → α