subsingleton_or_nnnorm_symm_pos — Mathlib

English

For a continuous linear equivalence e, either the domain E is subsingleton (trivial) or the inverse has positive norm: Subsingleton(E) ∨ 0 < ||e^{-1}||.

Русский

Для непрерывного линейного эквивалента e либо пространство E тривиально, либо обратный отображатель имеет положительную норму: Subsingleton(E) ∨ 0 < ||e^{-1}||.

LaTeX

$$$$(\\text{Subsingleton}(E)) \\lor 0 < \\|e^{-1}\\|.$$$$

Lean4

theorem subsingleton_or_nnnorm_symm_pos [RingHomIsometric σ₁₂] (e : E ≃SL[σ₁₂] F) :
    Subsingleton E ∨ 0 < ‖(e.symm : F →SL[σ₂₁] E)‖₊ :=
  subsingleton_or_norm_symm_pos e

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