le_def — Mathlib

English

For nonnegative rationals p and q, p ≤ q if and only if p.num · q.den ≤ q.num · p.den.

Русский

Для неотрицательных рациональных p и q верно: p ≤ q тогда и только тогда, когда p.num · q.den ≤ q.num · p.den.

LaTeX

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

Lean4

theorem le_def {p q : ℚ≥0} : p ≤ q ↔ p.num * q.den ≤ q.num * p.den := by rw [← NNRat.coe_le_coe, Rat.le_iff]; norm_cast

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