subsingleton_or_norm_symm_pos — Mathlib

English

The same positivity statement for NNReal-norm holds for the inverse of e: 0 < ||e^{-1}||_+.

Русский

Та же положительность для NNReal-нормы относится к обратному отображению e: 0 < ||e^{-1}||_+.

LaTeX

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

Lean4

theorem subsingleton_or_norm_symm_pos [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
    Subsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖ :=
  by
  rcases subsingleton_or_nontrivial E with (_i | _i)
  · left
    infer_instance
  · right
    exact e.norm_symm_pos

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