evalCLM — Mathlib

English

The evaluation functional at a point extends to a continuous linear map evalCLM: C(X, R)₀ →L[R] R, given by f ↦ f(x).

Русский

Оценочная функциональная карта в точке расширяет непрерывно-линейную карту evalCLM: C(X, R)₀ →L R, заданную f ↦ f(x).

LaTeX

$$$\operatorname{evalCLM}(x): C(X, R)₀ \to^L R,\quad f \mapsto f(x)$$$

Lean4

/-- The evaluation at a point, as a continuous linear map from `C(X, R)₀` to `R`. -/
def evalCLM (𝕜 : Type*) [Semiring 𝕜] [Module 𝕜 R] [ContinuousConstSMul 𝕜 R] (x : X) : C(X, R)₀ →L[𝕜] R :=
  (ContinuousMap.evalCLM 𝕜 x).comp (toContinuousMapCLM 𝕜)

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