lt_def — Mathlib

English

For nonnegative rationals p and q, p < q if and only if p.num · q.den < q.num · p.den (denominators are positive).

Русский

Для неотрицательных рациональных чисел p и q верно: p < q тогда и только тогда, когда p.num · q.den < q.num · p.den (знаменатели положительны).

LaTeX

$$$p < q \iff p.num \cdot q.den < q.num \cdot p.den$$$

Lean4

theorem lt_def {p q : ℚ≥0} : p < q ↔ p.num * q.den < q.num * p.den := by rw [← NNRat.coe_lt_coe, Rat.lt_iff]; norm_cast

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