isCompact — Mathlib

English

For quasispectrum, one can also obtain a compactness result: quasispectrum 𝕜 a is compact (as a space).

Русский

Для квази спектра также верно компактность: quasispectrum 𝕜 a — компактное пространство.

LaTeX

$$IsCompact(\\text{quasispectrum}_{\\mathbb{K}} a)$$

Lean4

@[simp]
theorem _root_.quasispectrum.isCompact (a : B) : IsCompact (quasispectrum 𝕜 a) :=
  by
  rw [Unitization.quasispectrum_eq_spectrum_inr' 𝕜 𝕜, ←
    AlgEquiv.spectrum_eq (WithLp.unitizationAlgEquiv 𝕜).symm (a : Unitization 𝕜 B)]
  exact spectrum.isCompact _

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