---

Step * of Lemma dyadic-scaled-rationals-dense

∀a:ℝ. ((r0 < a) ⇒ dense-in-interval((-∞, ∞);λr.∃n:ℤ. ∃m:ℕ+. (r = (r(n) * (a/r(2^m))))))
BY
{ (Auto THEN D 0 THEN Auto THEN Reduce 0 THEN RenameVar `c' (-3)) }

1
1. a : ℝ
2. r0 < a
3. c : {a:ℝ| a ∈ (-∞, ∞)} 
4. b : {r:ℝ| r ∈ (-∞, ∞)} 
5. c < b
⊢ ∃x:ℝ. (((c < x) ∧ (x < b)) ∧ (∃n:ℤ. ∃m:ℕ+. (x = (r(n) * (a/r(2^m))))))

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  ((r0  <  a)  {}\mRightarrow{}  dense-in-interval((-\minfty{},  \minfty{});\mlambda{}r.\mexists{}n:\mBbbZ{}.  \mexists{}m:\mBbbN{}\msupplus{}.  (r  =  (r(n)  *  (a/r(2\^{}m))))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  Reduce  0  THEN  RenameVar  `c'  (-3))

---

Home Index