English
Let v be a finite basis of E indexed by ι. For any function f: ι → F, there is a unique continuous linear map T: E → F such that T(v_i) = f(i) for all i ∈ ι; concretely, T( sum_i α_i v_i ) = sum_i α_i f(i).
Русский
Пусть v — конечный базис пространства E, индексированный множеством ι. Для любого отображения f: ι → F существует единственный непрерывно линейный переход T: E → F такой, что T(v_i) = f(i) для всех i; явление: T(∑_i α_i v_i) = ∑_i α_i f(i).
LaTeX
$$$\\exists!\\, T: E \\to_L[𝕜] F \\text{ с } T(v_i) = f(i) \\quad \\forall i \\in ι$$$
Lean4
/-- Construct a continuous linear map given the value at a finite basis. -/
def constrL (v : Basis ι 𝕜 E) (f : ι → F) : E →L[𝕜] F :=
haveI : FiniteDimensional 𝕜 E := FiniteDimensional.of_fintype_basis v
LinearMap.toContinuousLinearMap (v.constr 𝕜 f)
