subset_closedBall_norm

Mathlib.Analysis.Normed.Algebra.Spectrum

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

English

If [NormOneClass A], then σ(a) ⊆ closedBall(0,‖a‖).

Русский

Если [NormOneClass A], то σ(a) ⊆ замкнутый шар(0, ‖a‖).

LaTeX

$$$\\sigma_{\\mathbb{K}}(a) \\subseteq \\overline{B}_{\\mathbb{K}}(0, \\|a\\|).$$$

Lean4

theorem subset_closedBall_norm [NormOneClass A] (a : A) : σ a ⊆ Metric.closedBall (0 : 𝕜) ‖a‖ := fun k hk => by
  simp [norm_le_norm_of_mem hk]

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

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

Разделы

Аффилиация

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