compactSpace — Mathlib

English

If SpectrumRestricts a f, and the spectrum of S a is compact, then the spectrum of R a is also compact.

Русский

Если SpectrumRestricts a f и спектр S a компактен, то спектр R a также компактен.

LaTeX

$$$\\text{Compact}(\\mathrm{spectrum}(S,a)) \\Rightarrow \\text{Compact}(\\mathrm{spectrum}(R,a))$$$

Lean4

theorem compactSpace {R S A : Type*} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A]
    [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] {a : A} (f : C(S, R)) (h : SpectrumRestricts a f)
    [h_cpct : CompactSpace (spectrum S a)] : CompactSpace (spectrum R a) :=
  by
  rw [← isCompact_iff_compactSpace] at h_cpct ⊢
  exact h.image ▸ h_cpct.image (map_continuous f)

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