rpow_neg_one_le_rpow_neg_one — Mathlib

English

If a≥0, a ≤ b, and a is a unit, then b^(-1) ≤ a^(-1).

Русский

Если a≥0, a ≤ b, и a — единица, тогда b^(-1) ≤ a^(-1).

LaTeX

$$a \\ge 0, a \\le b, \\text{IsUnit}(a) \\Rightarrow b^{-1} \\le a^{-1}$$

Lean4

theorem rpow_neg_one_le_rpow_neg_one {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) :
    b ^ (-1 : ℝ) ≤ a ^ (-1 : ℝ) := by
  lift b to Aˣ using isUnit_of_le hau ha hab
  lift a to Aˣ using hau
  rw [rpow_neg_one_eq_inv a ha, rpow_neg_one_eq_inv b (ha.trans hab)]
  exact CStarAlgebra.inv_le_inv ha hab

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