div_lt_div_iff_mul_lt_mul — Mathlib

English

For integers a,b,c,d with b > 0 and d > 0, a/b < c/d if and only if a d < c b.

Русский

Для целых a,b,c,d с b > 0 и d > 0 выполняется: a/b < c/d тогда и только тогда, когда a d < c b.

LaTeX

$$$\\forall a,b,c,d \\in \\mathbb{Z},\\ b > 0 \\land d > 0 \\Rightarrow \\frac{a}{b} < \\frac{c}{d} \\iff a d < c b$$$

Lean4

theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) : (a : ℚ) / b < c / d ↔ a * d < c * b :=
  by
  simp only [lt_iff_le_not_ge]
  apply and_congr
  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
  · simp [div_def', Rat.divInt_le_divInt d_pos b_pos]

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