---

Step * of Lemma real-unit-ball-totally-bounded

∀n:ℕ. ∀k:ℕ+.  (∃L:{p:B(n)| rational-vec(n;p)}  List [(∀p:B(n). ∃i:ℕ||L||. (d(p;L[i]) ≤ (r1/r(k))))])
BY
{ (InstLemma `real-unit-ball-totally-bounded1` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (Assert finite(unit-ball-approx(n;k * 8 * n)) BY
               (Unfold `unit-ball-approx` 0
                THEN (BLemma `finite-decidable-subset` THEN Auto)
                THEN BLemma `finite-function`
                THEN Auto))
   THEN (RWO "finite-iff-listable" (-1)⋅ THENA Auto)
   THEN ExRepD) }

1
1. n : ℕ
2. k : ℕ+
3. ∀p:B(n). ∃q:unit-ball-approx(n;k * 8 * n). (d(p;approx-ball-to-ball(k * 8 * n;q)) ≤ (r1/r(k)))
4. L : unit-ball-approx(n;k * 8 * n) List
5. no_repeats(unit-ball-approx(n;k * 8 * n);L)
6. ∀x:unit-ball-approx(n;k * 8 * n). (x ∈ L)
⊢ ∃L:{p:B(n)| rational-vec(n;p)}  List [(∀p:B(n). ∃i:ℕ||L||. (d(p;L[i]) ≤ (r1/r(k))))]

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}k:\mBbbN{}\msupplus{}.    (\mexists{}L:\{p:B(n)|  rational-vec(n;p)\}    List  [(\mforall{}p:B(n).  \mexists{}i:\mBbbN{}||L||.  (d(p;L[i])  \mleq{}  (r1/r(k))))])


By

---

Latex:
(InstLemma  `real-unit-ball-totally-bounded1`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (Assert  finite(unit-ball-approx(n;k  *  8  *  n))  BY
                          (Unfold  `unit-ball-approx`  0
                            THEN  (BLemma  `finite-decidable-subset`  THEN  Auto)
                            THEN  BLemma  `finite-function`
                            THEN  Auto))
  THEN  (RWO  "finite-iff-listable"  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index