feat: add isCompact_{quasi}spectrum for instances of the continuous…

… functional calculus (#18117)

We already have instances for `CompactSpace`, but it's handy to have these when you need to work with the sets themselves (e.g., to show that `spectrum R a ∪ spectrum R b` is compact).

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

@@ -106,6 +106,11 @@ variable [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing
 variable [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A]
 variable [instCFCₙ : NonUnitalContinuousFunctionalCalculus R p]
 
+include instCFCₙ in
+lemma NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum (a : A) :
+    IsCompact (σₙ R a) :=
+  isCompact_iff_compactSpace.mpr inferInstance
+
 lemma NonUnitalStarAlgHom.ext_continuousMap [UniqueNonUnitalContinuousFunctionalCalculus R A]
     (a : A) (φ ψ : C(σₙ R a, R)₀ →⋆ₙₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ)
     (h : φ ⟨.restrict (σₙ R a) <| .id R, rfl⟩ = ψ ⟨.restrict (σₙ R a) <| .id R, rfl⟩) :

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -200,6 +200,11 @@ variable {R A : Type*} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpa
 variable [TopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A]
 variable [Algebra R A] [instCFC : ContinuousFunctionalCalculus R p]
 
+include instCFC in
+lemma ContinuousFunctionalCalculus.isCompact_spectrum (a : A) :
+    IsCompact (spectrum R a) :=
+  isCompact_iff_compactSpace.mpr inferInstance
+
 lemma StarAlgHom.ext_continuousMap [UniqueContinuousFunctionalCalculus R A]
     (a : A) (φ ψ : C(spectrum R a, R) →⋆ₐ[R] A) (hφ : Continuous φ) (hψ : Continuous ψ)
     (h : φ (.restrict (spectrum R a) <| .id R) = ψ (.restrict (spectrum R a) <| .id R)) :