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 _ _ _