innerSL_norm — Mathlib

English

The map e ↦ (w ↦ ⟨e, w⟩) from E into its dual has operator norm equal to 1.

Русский

Отображение e ↦ (w ↦ ⟨e, w⟩) из пространства E в его двойственное пространство имеет норму оператора равную 1.

LaTeX

$$$\|\mathrm{innerSL}_{\mathbb{K}}\| = 1$$$

Lean4

theorem innerSL_norm [Nontrivial E] : ‖(innerSL 𝕜 : E →L⋆[𝕜] E →L[𝕜] 𝕜)‖ = 1 :=
  show ‖(toDualMap 𝕜 E).toContinuousLinearMap‖ = 1 from LinearIsometry.norm_toContinuousLinearMap _

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