Theorems · Theorem · functional analysis

range_cfc_nnreal_subset

∀ {A : Type u_1} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [inst_4 : IsTopologicalRing A] [T2Space A] [inst_6 : PartialOrder A] [inst_7 : NonnegSpectrumClass ℝ A]
  [inst_8 : StarOrderedRing A] [inst_9 : ContinuousStar A] [inst_10 : StarModule ℝ A]
  [inst_11 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (0 ≤ a) range_cfc_nnreal_subset._auto_1 →
    (Set.range fun x => cfc x a) ⊆ {x | x ∈ StarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Cited by

1 results in Mathlib

Foundations

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

Assumes

RingStarRingAlgebraTopologicalSpaceIsTopologicalRingT2SpacePartialOrderNonnegSpectrumClassStarOrderedRingContinuousStarStarModuleContinuousFunctionalCalculus