---

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

∀n:ℕ. ∀k:ℕ+. ∀p:B(n).  ∃q:unit-ball-approx(n;k * 8 * n). (d(p;approx-ball-to-ball(k * 8 * n;q)) ≤ (r1/r(k)))
BY
{ (Auto THEN CaseNat 0 `n') }

1
1. n : ℕ
2. k : ℕ+
3. p : B(n)
4. n = 0 ∈ ℤ
⊢ ∃q:unit-ball-approx(0;k * 8 * 0). (d(p;approx-ball-to-ball(k * 8 * 0;q)) ≤ (r1/r(k)))

2
1. n : ℕ
2. k : ℕ+
3. p : B(n)
4. ¬(n = 0 ∈ ℤ)
⊢ ∃q:unit-ball-approx(n;k * 8 * n). (d(p;approx-ball-to-ball(k * 8 * n;q)) ≤ (r1/r(k)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}p:B(n).
    \mexists{}q:unit-ball-approx(n;k  *  8  *  n).  (d(p;approx-ball-to-ball(k  *  8  *  n;q))  \mleq{}  (r1/r(k)))


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index