---

Step * of Lemma dyadic-rationals-dense

No Annotations
dense-in-interval((-∞, ∞);λr.∃n:ℤ. ∃m:ℕ+. (r = (r(n)/r(2^m))))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN Reduce 0
   THEN (InstLemma `small-reciprocal-real`[ ⌜(b - a/r(2))⌝]⋅
         THENA (Auto THEN (MemTypeCD THEN Auto) THEN nRMul ⌜r(2)⌝ 0⋅ THEN Auto)
         )
   THEN D -1
   THEN (Assert (r1/r(2^k)) < (r1/r(k)) BY
               (BLemma `rless-int-fractions` THEN Auto THEN RW IntNormC 0 THEN Auto))) }

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

---

Latex:

---

Latex:
No  Annotations
dense-in-interval((-\minfty{},  \minfty{});\mlambda{}r.\mexists{}n:\mBbbZ{}.  \mexists{}m:\mBbbN{}\msupplus{}.  (r  =  (r(n)/r(2\^{}m))))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  Reduce  0
  THEN  (InstLemma  `small-reciprocal-real`[  \mkleeneopen{}(b  -  a/r(2))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto)
              )
  THEN  D  -1
  THEN  (Assert  (r1/r(2\^{}k))  <  (r1/r(k))  BY
                          (BLemma  `rless-int-fractions`  THEN  Auto  THEN  RW  IntNormC  0  THEN  Auto)))

---

Home Index