norm_id_of_nontrivial_seminorm — Mathlib

English

If the ambient space is normed and nontrivial, then the norm of the identity equals 1.

Русский

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

LaTeX

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

Lean4

/-- If there is an element with norm different from `0`, then the norm of the identity equals `1`.
(Since we are working with seminorms supposing that the space is non-trivial is not enough.) -/
theorem norm_id_of_nontrivial_seminorm (h : ∃ x : V, ‖x‖ ≠ 0) : ‖id V‖ = 1 :=
  le_antisymm (norm_id_le V) <| by
    let ⟨x, hx⟩ := h
    have := (id V).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

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