inclusionInDoubleDual_norm_eq — Mathlib

English

The operator norm of the canonical inclusion into the double dual equals the operator norm of the identity on the double dual space.

Русский

Пусть нормa оператора канонического включения в двойственный дуал равна норме тождественного отображения на двойственном дуале.

LaTeX

$$$\\|\\iota_E\\| = \\|\\mathrm{id}\\|$ in the appropriate operator-norm sense on the double dual.$$

Lean4

theorem inclusionInDoubleDual_norm_eq : ‖inclusionInDoubleDual 𝕜 E‖ = ‖ContinuousLinearMap.id 𝕜 (StrongDual 𝕜 E)‖ :=
  ContinuousLinearMap.opNorm_flip _

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