inv_le_inv_iff — Mathlib

English

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

Русский

В унитальной C*-алгебре, если 0 ≤ a ≤ b и a,b — единицы, то a⁻¹ ≤ b⁻¹ тогда и только тогда, когда b ≤ a.

LaTeX

$$0 ≤ a ≤ b \\;\\text{ and }\\; a,b \\in A^{\\times} \\Rightarrow a^{-1} ≤ b^{-1} \\iff b ≤ a$$

Lean4

/-- 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`. -/
protected theorem inv_le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (b : A)) : (↑a⁻¹ : A) ≤ b⁻¹ ↔ (b : A) ≤ a :=
  ⟨CStarAlgebra.inv_le_inv (inv_nonneg_of_nonneg a ha), CStarAlgebra.inv_le_inv hb⟩

Похожие утверждения