Theorems · Theorem · functional analysis

ContinuousOn.cfc_of_mem_nhdsSet

∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p]
  [ContinuousStar A] [CompleteSpace A] [inst_7 : TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X},
  s ∈ nhdsSet (⋃ x ∈ t, spectrum 𝕜 (a x)) →
    ContinuousOn a t →
      autoParam (∀ x ∈ t, p (a x)) ContinuousOn.cfc_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) ContinuousOn.cfc_of_mem_nhdsSet._auto_3 → ContinuousOn (fun x => cfc f (a x)) t

If f : 𝕜 → 𝕜 is continuous on s and a : X → A is continuous on t : Set X, and a x satisfies the predicate p associated to 𝕜 and s is a common neighborhood of the spectra of a x for all x ∈ t, then fun x ↦ cfc f (a x) is continuous on t. This is weaker than ContinuousOn.cfc since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using ContinuousOn.cfc and upperHemicontinuous_spectrum to produce the necessary family of compact sets.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

2 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarCompleteSpaceTopologicalSpace