div_le_iff_of_neg — Mathlib

English

If c < 0, then b/c ≤ a iff a c ≤ b.

Русский

Если c < 0, то b/c ≤ a эквивалентно a c ≤ b.

LaTeX

$$$c < 0 \rightarrow (\dfrac{b}{c} \le a \iff a c \le b)$$$

Lean4

theorem div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b :=
  ⟨fun h => div_mul_cancel₀ b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h hc.le, fun h =>
    calc
      a = a * c * (1 / c) := mul_mul_div a (ne_of_lt hc)
      _ ≥ b * (1 / c) := (mul_le_mul_of_nonpos_right h (one_div_neg.2 hc).le)
      _ = b / c := (div_eq_mul_one_div b c).symm⟩

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