inv_mul_le_iff — Mathlib

English

For x not equal to 0 and not equal to ∞, x⁻¹ y ≤ z iff y ≤ x z.

Русский

Для x, не равного 0 и не равного ∞, выполняется x⁻¹ y ≤ z ⇔ y ≤ x z.

LaTeX

$$$x \neq 0 \land x \neq \infty \Rightarrow (x^{-1} y \le z) \iff (y \le x z)$$$

Lean4

protected theorem inv_mul_le_iff {x y z : ℝ≥0∞} (h1 : x ≠ 0) (h2 : x ≠ ∞) : x⁻¹ * y ≤ z ↔ y ≤ x * z := by
  rw [← mul_le_mul_left h1 h2, ← mul_assoc, ENNReal.mul_inv_cancel h1 h2, one_mul]

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