compactSpace — Mathlib

English

If f is a continuous map from a spectrum restricting context S to R, and σ_S a is compact, then σ_R a is also compact.

Русский

Если f — непрерывное отображение из контекста спектра S к R, и σ_S a компактно, то σ_R a также компактно.

LaTeX

$$CompactSpace (σₙ S a) → CompactSpace (σₙ R a)$$

Lean4

theorem compactSpace {R S A : Type*} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A]
    [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] [TopologicalSpace R] [TopologicalSpace S] {a : A}
    (f : C(S, R)) (h : QuasispectrumRestricts a f) [h_cpct : CompactSpace (σₙ S a)] : CompactSpace (σₙ R a) :=
  by
  rw [← isCompact_iff_compactSpace] at h_cpct ⊢
  exact h.image ▸ h_cpct.image (map_continuous f)

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