norm_le_norm_of_mem

Mathlib.Analysis.Normed.Algebra.Spectrum

URI: https://scilib.ai/kg/mathlib#spectrum.norm_le_norm_of_mem

English

If k ∈ σ(a) and A has NormOneClass, then ‖k‖ ≤ ‖a‖.

Русский

Если k ∈ σ(a) и A имеет условие NormOneClass, то ‖k‖ ≤ ‖a‖.

LaTeX

$$$k \\in \\sigma(a) \\;\\Rightarrow\\; \\|k\\| \\leq \\|a\\|.$$$

Lean4

theorem norm_le_norm_of_mem [NormOneClass A] {a : A} {k : 𝕜} (hk : k ∈ σ a) : ‖k‖ ≤ ‖a‖ :=
  le_of_not_gt <| mt mem_resolventSet_of_norm_lt hk

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru