isCompact_spectrum — Mathlib

English

For any a in a C*-algebra that admits a continuous functional calculus, the spectrum of a is a compact subset of the base field.

Русский

Для элемента a в алгебре, на которую действует непрерывное функциональное исчисление, спектр a является компактным подмножеством основания.

LaTeX

$$$\\mathrm{spectrum}(R,a) \\text{ is compact}$$$

Lean4

theorem isCompact_spectrum (a : A) : IsCompact (spectrum R a) :=
  isCompact_iff_compactSpace.mpr inferInstance

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