spectralRadius_le_nnnorm — Mathlib

English

Spectral radius of a is bounded above by the norm of a, in suitable extended sense.

Русский

СПектральный радиус элемента a ограничен нормой элемента a в подходящем расширенном смысле.

LaTeX

$$spectralRadius 𝕜 a ≤ ‖a‖₊$$

Lean4

theorem spectralRadius_le_nnnorm [NormOneClass A] (a : A) : spectralRadius 𝕜 a ≤ ‖a‖₊ :=
  by
  refine iSup₂_le fun k hk => ?_
  exact mod_cast norm_le_norm_of_mem hk

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