toContinuousMapCLM — Mathlib

English

For each x ∈ X, the evaluation map ev_x: C(X, R)₀ → R, defined by ev_x(f) = f(x), is a continuous linear functional on C(X, R)₀.

Русский

Для каждого x ∈ X оценивание ev_x: C(X, R)₀ → R, задаваемое ev_x(f) = f(x), является непрерывной линейной функциональной картой на C(X, R)₀.

LaTeX

$$$\operatorname{ev}_x: C(X, R)₀ \to^L R,\quad \operatorname{ev}_x(f)=f(x)$$$

Lean4

/-- The coercion `C(X, R)₀ → C(X, R)` bundled as a continuous linear map. -/
@[simps]
def toContinuousMapCLM (M : Type*) [Semiring M] [Module M R] [ContinuousConstSMul M R] : C(X, R)₀ →L[M] C(X, R)
    where
  toFun f := f
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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