mem_resolventSet_of_spectralRadius_lt

English

If the spectral radius of a is smaller than ||k||, then k lies in the resolvent set of a.

Русский

Если спектральный радиус a меньше ||k||, то k принадлежит множеству резольвенты a.

LaTeX

$$$\text{If } \operatorname{spectralRadius}(\mathbb{K}, a) < \|k\|_{+}, \text{ then } k \in \rho(a).$$$

Lean4

theorem mem_resolventSet_of_spectralRadius_lt {a : A} {k : 𝕜} (h : spectralRadius 𝕜 a < ‖k‖₊) : k ∈ ρ a :=
  Classical.not_not.mp fun hn => h.not_ge <| le_iSup₂ (α := ℝ≥0∞) k hn

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