toLinearMap — Mathlib

English

From a bounded linear map f, one can recover its underlying linear map by forgetting continuity.

Русский

Из ограниченного линейного отображения f можно получить линейное отображение, забыв непрерывность.

LaTeX

$$$ \\text{toLinearMap} : IsBoundedLinearMap 𝕜 f \\to E \\to_{𝕜} F $$$

Lean4

/-- Construct a linear map from a function `f` satisfying `IsBoundedLinearMap 𝕜 f`. -/
def toLinearMap (f : E → F) (h : IsBoundedLinearMap 𝕜 f) : E →ₗ[𝕜] F :=
  IsLinearMap.mk' _ h.toIsLinearMap

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