instCompactSpaceNNReal — Mathlib

English

If A is NormedRing and Real-algebra, and σa is compact, then σℝ≥0 a is compact.

Русский

Если A — нормированное кольцо и алгебра над Real, и σa компактно, то σℝ≥0 a также компактно.

LaTeX

$$$\\text{CompactSpace}(\\sigma_{\\mathbb{R}_{\\ge 0}}(a)).$$$

Lean4

instance instCompactSpaceNNReal {A : Type*} [NormedRing A] [NormedAlgebra ℝ A] (a : A) [CompactSpace (spectrum ℝ a)] :
    CompactSpace (spectrum ℝ≥0 a) := by
  rw [← isCompact_iff_compactSpace] at *
  rw [← preimage_algebraMap ℝ]
  exact isClosed_nonneg.isClosedEmbedding_subtypeVal.isCompact_preimage <| by assumption

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