English
Construct a vector from a function f: Fin2 n → α by ofFn(f) = f; i.e., every such function corresponds to a vector of length n.
Русский
Пусть f: Fin2 n → α. Вектор с помощью ofFn(f) задаётся как f; то есть любая такая функция соответствует вектору длины n.
LaTeX
$$$ \mathrm{ofFn}(f) = f. $$$
Lean4
/-- Construct a vector from a function on `Fin2`. -/
abbrev ofFn (f : Fin2 n → α) : Vector3 α n :=
f