instCompactSpace

Mathlib.Analysis.Normed.Algebra.Spectrum

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

English

There is a canonical compact-space structure on the spectrum: CompactSpace (σ𝕜(a)).

Русский

Существует естественная структура компактного пространства на спектре: CompactSpace(σ𝕜(a)).

LaTeX

$$CompactSpace(\\sigma_{\\mathbb{K}}(a))$$

Lean4

instance instCompactSpace [ProperSpace 𝕜] (a : A) : CompactSpace (spectrum 𝕜 a) :=
  isCompact_iff_compactSpace.mp <| spectrum.isCompact a

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

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

Разделы

Аффилиация

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