ofFn — Mathlib

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

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