norm_id — Mathlib

English

If the domain is nontrivial, the operator norm of the identity map on a normed space is equal to 1.

Русский

Если пространство ненулевое, операторная норма тождественного отображения равна 1.

LaTeX

$$$\\|\\mathrm{id}_{E}\\| = 1.$$$

Lean4

/-- If a normed space is non-trivial, then the norm of the identity equals `1`. -/
@[simp]
theorem norm_id [Nontrivial E] : ‖ContinuousLinearMap.id 𝕜 E‖ = 1 :=
  by
  refine norm_id_of_nontrivial_seminorm ?_
  obtain ⟨x, hx⟩ := exists_ne (0 : E)
  exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩

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