toWOTCLM — Mathlib

English

The embedding from E →L[𝕜] F to E →WOT[𝕜] F is a continuous linear map.

Русский

Встраивание из E →L[𝕜] F в E →WOT[𝕜] F является непрерывно линейным отображением.

LaTeX

$$toWOTCLM : (E →L[𝕜] F) →L[𝕜] (E →WOT[𝕜] F)$$

Lean4

/-- The inclusion map from `E →[𝕜] F` to `E →WOT[𝕜] F`, bundled as a continuous linear map. -/
def toWOTCLM : (E →L[𝕜] F) →L[𝕜] (E →WOT[𝕜] F) :=
  ⟨LinearEquiv.toLinearMap (ContinuousLinearMap.toWOT 𝕜 E F), ContinuousLinearMap.continuous_toWOT⟩

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