---

Step * of Lemma rationals-dense-ext

∀x:ℝ. ∀y:{y:ℝ| x < y} .  ∃n:ℕ+. ∃m:ℤ. ((x < (r(m)/r(n))) ∧ ((r(m)/r(n)) < y))
BY
{ Extract of Obid: rationals-dense
  not unfolding  rlessw rdiv radd int-to-real mu
  finishing with Auto
  normalizes to:
  
  λx,y. eval n = rlessw(x;y) in
        <4 * n, (x n) + (y n), rlessw(x;(r((x n) + (y n))/r(4 * n))), rlessw((r((x n) + (y n))/r(4 * n));y)> }

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  x  <  y\}  .    \mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}m:\mBbbZ{}.  ((x  <  (r(m)/r(n)))  \mwedge{}  ((r(m)/r(n))  <  y))


By

---

Latex:
Extract  of  Obid:  rationals-dense
not  unfolding    rlessw  rdiv  radd  int-to-real  mu
finishing  with  Auto
normalizes  to:

\mlambda{}x,y.  eval  n  =  rlessw(x;y)  in
            ɜ  *  n
            ,  (x  n)  +  (y  n)
            ,  rlessw(x;(r((x  n)  +  (y  n))/r(4  *  n)))
            ,  rlessw((r((x  n)  +  (y  n))/r(4  *  n));y)>

---

Home Index