mul_sub_mul_div_mul_nonpos_iff — Mathlib

English

If c ≠ 0 and d ≠ 0, then (a d - b c)/(c d) ≤ 0 iff a/c ≤ b/d.

Русский

Если c ≠ 0 и d ≠ 0, то (a d - b c)/(c d) ≤ 0 тогда и только тогда a/c ≤ b/d.

LaTeX

$$(hc : c \neq 0) (hd : d \neq 0) : (a d - b c) / (c d) \le 0 \iff a / c \le b / d$$

Lean4

theorem mul_sub_mul_div_mul_nonpos_iff (hc : c ≠ 0) (hd : d ≠ 0) : (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d := by
  rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]

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