norm_le_norm_mul_of_mem

Mathlib.Analysis.Normed.Algebra.Spectrum

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

English

If k ∈ σ(a), then ‖k‖ ≤ ‖a‖·‖1‖.

Русский

Если k принадлежит спектру a, то ‖k‖ ≤ ‖a‖·‖1‖.

LaTeX

$$$k \\in \\sigma(a) \\;\\Longrightarrow\\; \\|k\\| \\leq \\|a\\| \\cdot \\|1\\|.$$$

Lean4

theorem norm_le_norm_mul_of_mem {a : A} {k : 𝕜} (hk : k ∈ σ a) : ‖k‖ ≤ ‖a‖ * ‖(1 : A)‖ :=
  le_of_not_gt <| mt mem_resolventSet_of_norm_lt_mul hk

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

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

Разделы

Аффилиация

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