le_inv_iff_mul_le — Mathlib

English

In ENNReal, a⁻¹ ≤ b if and only if 1 ≤ a·b under suitable nonzero/non-infinite conditions.

Русский

В ENNReal верно a⁻¹ ≤ b тогда и только если 1 ≤ a·b при соответствующих условиях на a и b.

LaTeX

$$$\\text{If appropriate conditions hold on } a,b, \\, a^{-1} \\le b \\iff 1 \\le a b$$$

Lean4

@[simp 900]
theorem le_inv_iff_mul_le : a ≤ b⁻¹ ↔ a * b ≤ 1 := by
  rw [← one_div, ENNReal.le_div_iff_mul_le] <;>
    · right
      simp

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