nnnorm_symm_pos — Mathlib

English

The nonnegative norm of the inverse, 0 < ||e^{-1}||_+, holds for the inverse of a continuous linear equivalence.

Русский

Для обратного отображения непрерывного линейного эквивалента выполняется 0 < ||e^{-1}||_+.

LaTeX

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

Lean4

theorem nnnorm_symm_pos [RingHomIsometric σ₁₂] [Nontrivial E] (e : E ≃SL[σ₁₂] F) : 0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊ :=
  e.norm_symm_pos

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