Theorems · Theorem · functional analysis

continuousOn_cfc_nnreal

∀ (A : Type u_2) [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal),
      autoParam (ContinuousOn f s) continuousOn_cfc_nnreal._auto_1 →
        ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum NNReal a ⊆ s}

A version of continuousOn_cfc over ℝ≥0 instead of RCLike 𝕜.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRingStarRingNormedAlgebraIsometricContinuousFunctionalCalculusContinuousStarPartialOrderStarOrderedRingNonnegSpectrumClassT2SpaceIsSemitopologicalRing