norm_single — Mathlib

English

Under nontriviality, the norm of the single projection is exactly one: ||ContinuousLinearMap.single 𝕜 E i|| = 1.

Русский

При условии не тривиальности норма оператора single равна единице: ||single|| = 1.

LaTeX

$$$$\\|\\mathrm{single}_{\\mathbb{K}}(i)\\| = 1.$$$$

Lean4

theorem norm_single [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] (i : ι) [Nontrivial (E i)] :
    ‖ContinuousLinearMap.single 𝕜 E i‖ = 1 :=
  (LinearIsometry.single 𝕜 E i).norm_toContinuousLinearMap

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