norm_id_of_nontrivial_seminorm — Mathlib

English

If the seminorm on the space is nontrivial, then the operator norm of the identity map on E is equal to 1.

Русский

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

LaTeX

$$$ \|\mathrm{id}_E\| = 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 : E, ‖x‖ ≠ 0) : ‖ContinuousLinearMap.id 𝕜 E‖ = 1 :=
  le_antisymm norm_id_le <| by
    let ⟨x, hx⟩ := h
    have := (ContinuousLinearMap.id 𝕜 E).ratio_le_opNorm x
    rwa [id_apply, div_self hx] at this

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