evalCLM — Mathlib

English

For each x in α, evaluation at x gives a continuous linear map from the space of continuous maps α → M to M, sending f to f(x).

Русский

Для каждого x в α эвалюация в точке x задаёт непрерывно-линейное отображение из пространства непрерывных функций α → M в M, то есть f ↦ f(x).

LaTeX

$$$\\mathrm{evalCLM}: \\alpha \\to_L[R] M, \\quad \\mathrm{evalCLM}(x)(f) = f(x).$$$

Lean4

/-- Evaluation at a point, as a continuous linear map. -/
@[simps apply]
def evalCLM (x : α) : C(α, M) →L[R] M where
  toFun f := f x
  map_add' _ _ := add_apply _ _ x
  map_smul' _ _ := smul_apply _ _ x

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