evalCLM — Mathlib

English

There is a natural linear map forgetting the boundedness: (α →ᵇ β) → C(α, β), linear over 𝕜.

Русский

Существует естественное линейное отображение от ограниченно непрерывных функций к непрерывным отображениям: (α →ᵇ β) → C(α,β), линейное по 𝕜.

LaTeX

$$$toContinuousMapLinearMap : (\\alpha \\to^{\\mathrm{b}} \\beta) \\to_{L[\\mathbb{K}]} C(\\alpha,\\beta)$$$

Lean4

/-- The evaluation at a point, as a continuous linear map from `α →ᵇ β` to `β`. -/
@[simps]
def evalCLM (x : α) : (α →ᵇ β) →L[𝕜] β where
  toFun f := f x
  map_add' _ _ := add_apply _ _ _
  map_smul' _ _ := smul_apply _ _ _

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