Theorems · Theorem · functional analysis

continuousOn_cfc

∀ {𝕜 : 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] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : 𝕜 → 𝕜),
      autoParam (ContinuousOn f s) continuousOn_cfc._auto_1 → ContinuousOn (cfc f) {a | p a ∧ spectrum 𝕜 a ⊆ s}

For f : 𝕜 → 𝕜 continuous on a compact set s, cfc f is continuous on the set of a : A satisfying the predicate p (associated to 𝕜) and whose 𝕜-spectrum is contained in s.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

4 results in Mathlib

Foundations

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

Assumes

RCLikeNormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStar