norm_pos — Mathlib

English

For a nontrivial normed space E and a continuous linear equivalence e, the operator norm of e is strictly positive: 0 < ||e||.

Русский

Для не тривиального нормированного пространства E и непрерывного линейного эквивалента e норма оператора e строго положительна: 0 < ||e||.

LaTeX

$$$$0 < \\|e\\|.$$$$

Lean4

theorem norm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e : E →SL[σ₁₂] F)‖ :=
  pos_of_mul_pos_left (lt_of_lt_of_le zero_lt_one e.one_le_norm_mul_norm_symm) (norm_nonneg _)

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