Theorems · Theorem · functional analysis

cfc_map_pi

∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : CommRing S]
  [inst_6 : Algebra R S] [inst_7 : (i : ι) → Ring (A i)] [inst_8 : (i : ι) → Algebra S (A i)]
  [inst_9 : (i : ι) → Algebra R (A i)] [∀ (i : ι), IsScalarTower R S (A i)] [hinst : IsScalarTower R S ((i : ι) → A i)]
  [inst_11 : (i : ι) → StarRing (A i)] [inst_12 : (i : ι) → TopologicalSpace (A i)] {p : ((i : ι) → A i) → Prop}
  {q : (i : ι) → A i → Prop} [inst_13 : ContinuousFunctionalCalculus R ((i : ι) → A i) p]
  [inst_14 : ∀ (i : ι), ContinuousFunctionalCalculus R (A i) (q i)] [∀ (i : ι), ContinuousMap.UniqueHom R (A i)]
  (f : R → R) (a : (i : ι) → A i),
  autoParam (ContinuousOn f (⋃ i, spectrum R (a i))) cfc_map_pi._auto_1 →
    autoParam (p a) cfc_map_pi._auto_3 →
      autoParam (∀ (i : ι), q i (a i)) cfc_map_pi._auto_5 → cfc f a = fun i => cfc f (a i)

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarCommRingAlgebraRingAlgebraAlgebraIsScalarTowerIsScalarTowerStarRingTopologicalSpaceContinuousFunctionalCalculusContinuousFunctionalCalculusContinuousMap.UniqueHom