div_lt_div'' — Mathlib

English

If a < b and c < d in an ordered commutative group, then a/d < b/c.

Русский

Если a < b и c < d в упорядоченной коммутативной группе, то a/d < b/c.

LaTeX

$$$(a < b) \land (c < d) \implies \dfrac{a}{d} < \dfrac{b}{c}$$$

Lean4

@[to_additive (attr := gcongr) sub_lt_sub]
theorem div_lt_div'' (hab : a < b) (hcd : c < d) : a / d < b / c :=
  by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]
  exact mul_lt_mul_of_lt_of_lt hab hcd

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