Rational approximation in nonnegative reals

This module records the density of nonnegative rationals in ℝ≥0 in the form used for countable rational approximations of real-valued constructions.

theorem BGW.Probability.exists_nnrat_btwn {a b : NNReal} (h : a < b) : ∃ (q : ℚ≥0), a < ↑q ∧ ↑q < b

Every strict inequality between nonnegative reals has a nonnegative rational strictly between its endpoints.