Theorems · Theorem · functional analysis

Unitization.inr_le_iff

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a b : A),
  autoParam (IsSelfAdjoint a) Unitization.inr_le_iff._auto_1 →
    autoParam (IsSelfAdjoint b) Unitization.inr_le_iff._auto_3 → (↑a ≤ ↑b ↔ a ≤ b)

Defined in: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
Cited by: 8 results in Mathlib
Foundations: Depth 317 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NonUnitalCStarAlgebra PartialOrder StarOrderedRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites16

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

Setproof · cited by 53,352
Realproof · cited by 25,697
PartialOrderstatement and proof · cited by 6,410
Complexstatement and proof · cited by 5,565
StarOrderedRingstatement and proof · cited by 587
IsSelfAdjointstatement and proof · cited by 545
spectrumproof · cited by 510
Unitizationstatement and proof · cited by 220
sub_nonnegproof · cited by 167
NonUnitalCStarAlgebrastatement and proof · cited by 149
Unitization.inrstatement and proof · cited by 109
IsSelfAdjoint.subproof · cited by 13

Cited by8

Results whose statement or proof uses this declaration.

Unitization.inr_nonneg_iffproof · cited by 8
CStarAlgebra.norm_le_norm_of_nonneg_of_leproof · cited by 6
CFC.monotoneOn_one_sub_one_add_invproof · cited by 2
Unitization.convexOn_of_convexOn_inr_compproof · cited by 1
CStarAlgebra.star_left_conjugate_le_norm_smulproof · cited by 1
IsStarProjection.mul_right_and_mul_left_of_nonneg_of_leproof · cited by 1
CStarAlgebra.norm_sub_mul_self_le_of_inrproof · cited by 0
Unitization.concaveOn_of_concaveOn_inr_compproof · cited by 0