continuousLinearMapToWeakDual — Mathlib

English

There is a continuous linear map from StrongDual to WeakDual implementing the identity on the underlying vector spaces.

Русский

Существует непрерывное линейное отображение от StrongDual к WeakDual, реализующее тождественный переход между пространствами.

LaTeX

$$$continuousLinearMapToWeakDual : StrongDual 𝕜 E \\toL[𝕜] WeakDual 𝕜 E$$$

Lean4

/-- For a normed space `E`, according to `toWeakDual_continuous` the "identity mapping"
`StrongDual 𝕜 E → WeakDual 𝕜 E` is continuous. This definition implements it as a continuous linear
map. -/
def continuousLinearMapToWeakDual : StrongDual 𝕜 E →L[𝕜] WeakDual 𝕜 E :=
  { StrongDual.toWeakDual with cont := toWeakDual_continuous }

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