Comparing fractions of natural numbers in ℝ≥0∞

A probability computed by counting is a fraction a / b of natural numbers in ℝ≥0∞. Comparing two such fractions reduces to comparing the cross products in ℕ.

Main results

• ENNReal.natCast_div_le_natCast_div_iff: for b, d ≠ 0, a / b ≤ c / d ↔ a * d ≤ c * b.

theorem ENNReal.natCast_div_le_natCast_div_iff {a b c d : ℕ} (hb : b ≠ 0) (hd : d ≠ 0) : ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

Two fractions of natural numbers with nonzero denominators compare in ℝ≥0∞ as their cross products compare in ℕ: a / b ≤ c / d ↔ a * d ≤ c * b.