div_le_div_iff' — Mathlib

English

For a,b,c,d ∈ α, a / b ≤ c / d ↔ a d ≤ c b.

Русский

Для элементов a,b,c,d: a / b ≤ c / d эквивалентно a d ≤ c b.

LaTeX

$$$a / b \le c / d \iff a d \le c b$$$

Lean4

/-- See also `div_le_div_iff` for a version that works for `LinearOrderedSemifield` with
additional assumptions. -/
@[to_additive sub_le_sub_iff]
theorem div_le_div_iff' : a / b ≤ c / d ↔ a * d ≤ c * b := by simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'

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