mul_le_iff_le_inv — Mathlib

English

For ENNReal, r*a ≤ b ↔ a ≤ r⁻¹·b under r ≠ 0, r ≠ ∞.

Русский

Для ENNReal, r a ≤ b эквивалентно a ≤ r⁻¹ b при r ≠ 0 и r ≠ ∞.

LaTeX

$$$r \\neq 0, \\; r \\neq \\infty \\Rightarrow r a \\le b \\iff a \\le r^{-1} b$$$

Lean4

theorem mul_le_iff_le_inv {a b r : ℝ≥0∞} (hr₀ : r ≠ 0) (hr₁ : r ≠ ∞) : r * a ≤ b ↔ a ≤ r⁻¹ * b := by
  rw [← @ENNReal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, ENNReal.mul_inv_cancel hr₀ hr₁, one_mul]

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