inclusionInDoubleDualLi — Mathlib

English

The canonical inclusion map is an isometry with closed image into the double dual.

Русский

Каноническое вложение является изометрией с замкнутым образом в двойственном дуале.

LaTeX

$$$\\iota_E : E \\to (E^*)^*$ является изометрией и образ его замкнуто.$$

Lean4

/-- The inclusion of a normed space in its double strong dual is an isometry onto its image. -/
def inclusionInDoubleDualLi : E →ₗᵢ[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E) :=
  { inclusionInDoubleDual 𝕜 E with
    norm_map' := by
      intro x
      apply le_antisymm
      · exact double_dual_bound 𝕜 E x
      rw [ContinuousLinearMap.norm_def]
      refine le_csInf ContinuousLinearMap.bounds_nonempty ?_
      rintro c ⟨hc1, hc2⟩
      exact norm_le_dual_bound 𝕜 x hc1 hc2 }

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