English
Same order criterion as 43080 but with a general a and b as units, giving an inequality equivalent to a ≤ b in terms of norms of products of square roots.
Русский
Та же критерий порядка, но здесь a и b — единицы; неравенство эквивалентно условию по норме произведения квадратных корней.
LaTeX
$$a ≤ b \\iff \\|\\sqrt a \\cdot \\sqrt{b^{-1}}\\| ≤ 1$$
Lean4
/-- In a unital C⋆-algebra, if `0 ≤ a ≤ b` and `a` and `b` are units, then `b⁻¹ ≤ a⁻¹`. -/
protected theorem inv_le_inv {a b : Aˣ} (ha : 0 ≤ (a : A)) (hab : (a : A) ≤ b) : (↑b⁻¹ : A) ≤ a⁻¹ :=
by
have hb := ha.trans hab
have hb_inv : (0 : A) ≤ b⁻¹ := inv_nonneg_of_nonneg b hb
have ha_inv : (0 : A) ≤ a⁻¹ := inv_nonneg_of_nonneg a ha
rw [le_iff_norm_sqrt_mul_sqrt_inv ha hb, ← sq_le_one_iff₀ (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self] at hab
rw [le_iff_norm_sqrt_mul_sqrt_inv hb_inv ha_inv, inv_inv, ← sq_le_one_iff₀ (norm_nonneg _), sq, ←
CStarRing.norm_self_mul_star]
rwa [star_mul, IsSelfAdjoint.of_nonneg (sqrt_nonneg _), IsSelfAdjoint.of_nonneg (sqrt_nonneg _)] at hab ⊢
