isCompact_quasispectrum

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital

URI: https://scilib.ai/kg/mathlib#NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum

English

The quasispectrum σₙ R a of any a in a nonunital calculus is compact.

Русский

Квазиспектр σₙ R a элемента a в неединичном калькуляторе компактен.

LaTeX

$$IsCompact (σₙ R a)$$

Lean4

theorem isCompact_quasispectrum (a : A) : IsCompact (σₙ R a) :=
  isCompact_iff_compactSpace.mpr inferInstance

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

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

Разделы

Аффилиация

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