instCompactSpaceNNReal — Mathlib

English

If a is an algebra over Real and σa is compact, then σℝ≥0a is compact; hence the NNReal spectrum is closed in its ambient topology.

Русский

Если a — алгебра над Real и σa компактно, то σℝ≥0a компактно; следовательно, спектр NNReal замкнут в своей топологии.

LaTeX

$$IsCompact(\\sigma_{\\mathbb{R}_{≥0}}(a))$$

Lean4

instance _root_.quasispectrum.instCompactSpaceNNReal [NormedSpace ℝ B] [IsScalarTower ℝ B B] [SMulCommClass ℝ B B]
    (a : B) [CompactSpace (quasispectrum ℝ a)] : CompactSpace (quasispectrum ℝ≥0 a) :=
  by
  rw [← isCompact_iff_compactSpace] at *
  rw [← quasispectrum.preimage_algebraMap ℝ]
  exact isClosed_nonneg.isClosedEmbedding_subtypeVal.isCompact_preimage <| by assumption

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