Theorems · Theorem · functional analysis

IsometricContinuousFunctionalCalculus.isGreatest_spectrum

∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A]
  (a : A),
  autoParam (0 ≤ a) IsometricContinuousFunctionalCalculus.isGreatest_spectrum._auto_1 →
    IsGreatest (spectrum NNReal a) ‖a‖₊

Defined in: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
Cited by: 1 results in Mathlib
Foundations: Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedRing StarRing NormedAlgebra PartialOrder StarOrderedRing IsometricContinuousFunctionalCalculus NonnegSpectrumClass Nontrivial

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites19

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

Realstatement and proof · cited by 25,697
PartialOrderstatement and proof · cited by 6,410
NNRealstatement and proof · cited by 4,310
Nontrivialstatement and proof · cited by 2,416
StarRingstatement and proof · cited by 1,686
NormedAlgebrastatement and proof · cited by 1,165
NNNorm.nnnormstatement and proof · cited by 952
NormedRingstatement and proof · cited by 924
StarOrderedRingstatement and proof · cited by 587
IsSelfAdjointstatement and proof · cited by 545
Set.image_congrproof · cited by 533
spectrumstatement and proof · cited by 510

Cited by1

Results whose statement or proof uses this declaration.

MonotoneOn.nnnorm_cfcproof · cited by 0