exists_nnnorm_eq_spectralRadius — Mathlib

English

In the complex spectrum of a, there exists z in spectrum(ℂ, a) such that ‖z‖₊ = ρ(ℂ, a).

Русский

В спектре комплексного банахова алгебраического элемента a существует z ∈ spectrum(ℂ, a) такое, что ‖z‖₊ = ρ(ℂ, a).

LaTeX

$$$\\exists z \\in \\mathrm{spectrum}_{\\mathbb{C}}(a) : \\|z\\|_{+} = \\rho_{\\mathbb{C}}(a)$$$

Lean4

/-- In a complex Banach algebra, the spectral radius is always attained by some element of the
spectrum. -/
theorem exists_nnnorm_eq_spectralRadius (a : A) : ∃ z ∈ spectrum ℂ a, (‖z‖₊ : ℝ≥0∞) = spectralRadius ℂ a :=
  exists_nnnorm_eq_spectralRadius_of_nonempty (spectrum.nonempty a)

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