norm_symm_pos — Mathlib

English

The operator norm of the inverse map e^{-1} is strictly positive: 0 < ||e^{-1}||.

Русский

Норма оператора обратного отображения e^{-1} строго положительна: 0 < ||e^{-1}||.

LaTeX

$$$$0 < \\|e^{-1}\\|.$$$$

Lean4

theorem norm_symm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e.symm : F →SL[σ₂₁] E)‖ :=
  pos_of_mul_pos_right (zero_lt_one.trans_le e.one_le_norm_mul_norm_symm) (norm_nonneg _)

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