Theorems · Theorem · functional analysis

SpectrumRestricts.nnreal_add

∀ {A : Type u_1} [inst : CStarAlgebra A] {a b : A},
  IsSelfAdjoint a →
    IsSelfAdjoint b →
      SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
        SpectrumRestricts b ⇑ContinuousMap.realToNNReal → SpectrumRestricts (a + b) ⇑ContinuousMap.realToNNReal

Defined in: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 312 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CStarAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites20

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
Algebra.algebraMapproof · cited by 4,706
NNRealstatement · cited by 4,310
LE.le.transproof · cited by 3,151
ContinuousMapstatement · cited by 2,491
le_reflproof · cited by 2,061
NNReal.toRealproof · cited by 1,260
map_addproof · cited by 964
NNNorm.nnnormproof · cited by 952
add_le_addproof · cited by 666
IsSelfAdjointstatement and proof · cited by 545

Cited by2

Results whose statement or proof uses this declaration.

spectrum_star_mul_self_nonnegproof · cited by 1
CStarAlgebra.spectralOrderedRingproof · cited by 1