Theorems · Theorem · functional analysis

continuousWithinAt_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}
  {s : Set X},
  TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (spectrum R a) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (spectrum R a)) → ContinuousWithinAt (fun x => cfc (f x) a) s x₀

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

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarRingStarRingTopologicalSpaceAlgebraContinuousFunctionalCalculusTopologicalSpace