norm_id — Mathlib

English

For any normed additive group space, the norm of the identity is 1 when the space is nontrivial.

Русский

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

LaTeX

$$$$ \|\mathrm{id}\!_V\| = 1 $$$$

Lean4

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

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