toWeakSpaceCLM — Mathlib

English

There is a canonical continuous linear map from E to WeakSpace 𝕜 E implementing the identity embedding.

Русский

Существует каноничное непрерывное линейное отображение из E в WeakSpace 𝕜 E, реализующее тождественное вложение.

LaTeX

$$$toWeakSpaceCLM : E \\toL[𝕜] \\mathrm{WeakSpace} 𝕜 E$$$

Lean4

/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
This definition implements it as a continuous linear map. -/
def toWeakSpaceCLM : E →L[𝕜] WeakSpace 𝕜 E where
  __ := toWeakSpace 𝕜 E
  cont := by
    apply WeakBilin.continuous_of_continuous_eval
    exact ContinuousLinearMap.continuous

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