basisFun — Mathlib

English

There is a canonical basis for the space of functions η → R, indexed by η, where the i-th basis vector is the function that takes value 1 at i and 0 elsewhere.

Русский

Существует канонический базис пространства функций η → R, индексируемый по η; i-й базисный вектор — функция, принимающая значение 1 в точке i и значение 0 в остальных точках.

LaTeX

$$$\text{basisFun } R η :\; \text{Basis } η R (η \to R)$$$

Lean4

/-- The basis on `η → R` where the `i`th basis vector is `Function.update 0 i 1`. -/
noncomputable def basisFun : Basis η R (η → R) :=
  Basis.ofEquivFun (LinearEquiv.refl _ _)

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