le_inv_iff — Mathlib

English

For positive units a,b, a ≤ b if and only if b⁻¹ ≤ a⁻¹.

Русский

Для положительных единиц a,b верно: a ≤ b тогда и только тогда, когда b⁻¹ ≤ a⁻¹.

LaTeX

$${a,b : A^{\\times}} (ha : 0 ≤ a) (hb : 0 ≤ b) : a^{-1} ≤ b \\iff b^{-1} ≤ a$$

Lean4

theorem le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) : a ≤ (↑b⁻¹ : A) ↔ b ≤ (↑a⁻¹ : A) := by
  simpa using CStarAlgebra.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb

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