English
Let α be a topological space and M a topological vector space over a semiring R. There is a natural R-linear map that sends a continuous function f: α → M to its evaluation at each point, i.e. a LinearMap from C(α, M) to α → M given by f ↦ (x ↦ f(x)).
Русский
Пусть α — топологическое пространство, M — топологическое векторное пространство над кольцом R. Существует естественный линейный по R отображение, которое переводит непрерывную функцию f: α → M в её значения в каждой точке, то есть линейное отображение от C(α, M) к α → M, определяемое f ↦ (x ↦ f(x)).
LaTeX
$$$\\operatorname{coeFnLinearMap}: C(\\alpha,M) \\to_L[R] (\\alpha \\to M), \\quad \\operatorname{coeFnLinearMap}(f) = (x \\mapsto f(x)).$$$
Lean4
/-- Coercion to a function as a `LinearMap`. -/
@[simps]
def coeFnLinearMap : C(α, M) →ₗ[R] α → M :=
{ (coeFnAddMonoidHom : C(α, M) →+ _) with map_smul' := coe_smul }
