spectralRadius_mem_spectrum — Mathlib

English

If spectrum is nonempty and SpectrumRestricts holds with Real embedding, then the real spectral radius lies in the spectrum.

Русский

Если спектр не пуст и выполняется ограничение спектра на Real-встраивание, то вещественный спектр принадлежит спектру.

LaTeX

$$spectralRadius Real a).toReal ∈ spectrum Real a$$

Lean4

theorem _root_.Real.spectralRadius_mem_spectrum {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] {a : A}
    (ha : (spectrum ℝ a).Nonempty) (ha' : SpectrumRestricts a ContinuousMap.realToNNReal) :
    (spectralRadius ℝ a).toReal ∈ spectrum ℝ a :=
  NNReal.spectralRadius_mem_spectrum ha ha'

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