div_mul_le_div_mul_of_div_le_div — Mathlib

English

If a/b ≤ c/d and e ≥ 0, then a/(b e) ≤ c/(d e).

Русский

Если a/b ≤ c/d и e ≥ 0, то a/(b e) ≤ c/(d e).

LaTeX

$$$\left(\frac{a}{b} \le \frac{c}{d}\right) \land (0 \le e) \Rightarrow \frac{a}{b e} \le \frac{c}{d e}$$$

Lean4

theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) : a / (b * e) ≤ c / (d * e) :=
  by
  rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]
  exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 he)

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