monotonicity of a ↦ a⁺ on commuting elements in a C⋆-algebra

theorem ContinuousMap.realToRCLike_posPart {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, ℝ)) : (realToRCLike ℂ f)⁺ = realToRCLike ℂ f⁺

theorem ContinuousMap.realToRCLike_negPart {X : Type u_1} [TopologicalSpace X] [CompactSpace X] (f : C(X, ℝ)) : (realToRCLike ℂ f)⁻ = realToRCLike ℂ f⁻

theorem CStarAlgebra.posPart_mono (A : Type u_1) [NonUnitalCommCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Monotone fun (a : A) => a⁺

In a commutative C⋆-algebra, the positive part map fun a ↦ a⁺ is monotone.

theorem CStarAlgebra.negPart_anti (A : Type u_1) [NonUnitalCommCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Antitone fun (a : A) => a⁻

In a commutative C⋆-algebra, the negative part map fun a ↦ a⁻ is antitone.

theorem CStarAlgebra.Commute.posPart_mono {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : Commute a b) (hle : a ≤ b) (ha : IsSelfAdjoint a := by cfc_tac) (hb : IsSelfAdjoint b := by cfc_tac) : a⁺ ≤ b⁺

The positive part map fun a ↦ a⁺ is monotone on commuting selfadjoint elements in a C⋆-algebra

theorem CStarAlgebra.Commute.negPart_anti {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : Commute a b) (hle : a ≤ b) (ha : IsSelfAdjoint a := by cfc_tac) (hb : IsSelfAdjoint b := by cfc_tac) : b⁻ ≤ a⁻

The negative part map fun a ↦ a⁻ is antitone on commuting selfadjoint elements in a C⋆-algebra