Theorems · Theorem · functional analysis

continuousOn_cfc_setProd_nhdsSet

∀ {𝕜 : 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] {s : Set 𝕜},
  ContinuousOn (fun fa => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((UniformOnFun.toFun {t | IsCompact t ∧ t ⊆ s}) f) s} ×ˢ {a | p a ∧ s ∈ nhdsSet (spectrum 𝕜 a)})

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

0 results in Mathlib

Foundations

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

Assumes

RCLikeNormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarCompleteSpace