Theorems · Definition · functional analysis

cfcHomSuperset

{R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : Ring A] →
                  [inst_6 : StarRing A] →
                    [inst_7 : TopologicalSpace A] →
                      [inst_8 : Algebra R A] →
                        [instCFC : ContinuousFunctionalCalculus R A p] →
                          {a : A} → p a → {s : Set R} → spectrum R a ⊆ s → C(↑s, R) →⋆ₐ[R] A

The composition of cfcHom with the natural embedding C(s, R) → C(spectrum R a, R) whenever spectrum R a ⊆ s. This is sometimes necessary in order to consider the same continuous functions applied to multiple distinct elements, with the added constraint that cfc does not suffice. This can occur, for example, if it is necessary to use uniqueness of this continuous functional calculus.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringStarRingMetricSpaceIsTopologicalSemiringContinuousStarRingStarRingTopologicalSpaceAlgebraContinuousFunctionalCalculus