Theorems · Theorem · functional analysis

cfc_map_prod

∀ {A : Type u_1} {B : Type u_2} {R : Type u_3} {S : 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 : Ring A] [inst_8 : Ring B] [inst_9 : Algebra S A] [inst_10 : Algebra S B]
  [inst_11 : Algebra R A] [inst_12 : Algebra R B] [IsScalarTower R S A] [IsScalarTower R S B] [inst_15 : StarRing A]
  [inst_16 : StarRing B] [inst_17 : TopologicalSpace A] [inst_18 : TopologicalSpace B] {pab : A × B → Prop}
  {pa : A → Prop} {pb : B → Prop} [inst_19 : ContinuousFunctionalCalculus R (A × B) pab]
  [inst_20 : ContinuousFunctionalCalculus R A pa] [inst_21 : ContinuousFunctionalCalculus R B pb]
  [ContinuousMap.UniqueHom R A] [ContinuousMap.UniqueHom R B] (f : R → R) (a : A) (b : B),
  autoParam (ContinuousOn f (spectrum R a ∪ spectrum R b)) cfc_map_prod._auto_1 →
    autoParam (pab (a, b)) cfc_map_prod._auto_3 →
      autoParam (pa a) cfc_map_prod._auto_5 → autoParam (pb b) cfc_map_prod._auto_7 → cfc f (a, b) = (cfc f a, cfc f b)

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

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarCommRingAlgebraRingRingAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerStarRingStarRingTopologicalSpaceTopologicalSpaceContinuousFunctionalCalculusContinuousFunctionalCalculusContinuousFunctionalCalculusContinuousMap.UniqueHomContinuousMap.UniqueHom