Theorems · Theorem · functional analysis

continuousAt_cfc_fun

∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A]
  [inst_6 : StarRing A] [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A]
  [inst_9 : ContinuousFunctionalCalculus R A p] [inst_10 : TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X},
  TendstoUniformlyOn f (f x₀) (nhds x₀) (spectrum R a) →
    (∀ᶠ (x : X) in nhds x₀, ContinuousOn (f x) (spectrum R a)) → ContinuousAt (fun x => cfc (f x) a) x₀

If f : X → R → R tends to f x₀ uniformly (along 𝓝 x₀) on the spectrum of a, and each f x is continuous on the spectrum of a, then fun x ↦ cfc (f x) a is continuous at x₀.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarRingStarRingTopologicalSpaceAlgebraContinuousFunctionalCalculusTopologicalSpace