Theorems · Theorem · functional analysis

continuous_cfcHomSuperset_left

∀ {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] [inst_6 : TopologicalSpace X] {s : Set 𝕜},
  IsCompact s →
    ∀ (f : C(↑s, 𝕜)) (a : X → A),
      Continuous a →
        ∀ (ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s)
          (ha' : autoParam (∀ (x : X), p (a x)) continuous_cfcHomSuperset_left._auto_1),
          Continuous fun x => (cfcHomSuperset ⋯ ⋯) f

cfcHomSuperset is continuous in the variable a : A when s : Set 𝕜 is compact and a varies over elements whose spectrum is contained in s, all of which satisfy the predicate p.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarTopologicalSpace