Theorems · Theorem · functional analysis

CStarAlgebra.inv_le_inv_iff

∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : Aˣ},
  0 ≤ ↑a → 0 ≤ ↑b → (↑a⁻¹ ≤ ↑b⁻¹ ↔ ↑b ≤ ↑a)

In a unital C⋆-algebra, if 0 ≤ a and 0 ≤ b and a and b are units, then a⁻¹ ≤ b⁻¹ if and only if b ≤ a.

Defined in

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Cited by

2 results in Mathlib

Foundations

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

Assumes

CStarAlgebraPartialOrderStarOrderedRing