---

Step * 1 1 of Lemma approx-fixpoint-unit-ball-0


1. n : ℕ+
2. f : B(n) ⟶ B(n)
3. ¬(∀x:B(n). f x ≠ x)
4. e : {e:ℝ| r0 < e} 
5. r0 < (e/r(3))
6. t : ∀p:B(n). (((r(2) * e/r(3)) < d(f p;p)) ∨ (d(f p;p) < e))
7. ∀p:B(n). ((↑isr(t p)) ⇒ (d(f p;p) < e))
8. ∀p:B(n). ((¬↑isr(t p)) ⇒ ((r(2) * e/r(3)) < d(f p;p)))
9. del : {del:ℝ| r0 < del} 
10. ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < (e/r(3))))
11. k : ℕ+
12. ((r1/r(k)) < del) ∧ ((r1/r(k)) < (e/r(3)))
⊢ ↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑isr(t approx-ball-to-ball(k;q)))
BY
{ ((InstLemma `real-unit-ball-totally-bounded1` [⌜n⌝;⌜k⌝]⋅ THENA Auto) THEN D 0 THEN D 0 With ⌜k * 8 * n⌝  THEN Auto) }

1
1. n : ℕ+
2. f : B(n) ⟶ B(n)
3. ¬(∀x:B(n). f x ≠ x)
4. e : {e:ℝ| r0 < e} 
5. r0 < (e/r(3))
6. t : ∀p:B(n). (((r(2) * e/r(3)) < d(f p;p)) ∨ (d(f p;p) < e))
7. ∀p:B(n). ((↑isr(t p)) ⇒ (d(f p;p) < e))
8. ∀p:B(n). ((¬↑isr(t p)) ⇒ ((r(2) * e/r(3)) < d(f p;p)))
9. del : {del:ℝ| r0 < del} 
10. ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < (e/r(3))))
11. k : ℕ+
12. (r1/r(k)) < del
13. (r1/r(k)) < (e/r(3))
14. ∀p:B(n). ∃q:unit-ball-approx(n;k * 8 * n). (d(p;approx-ball-to-ball(k * 8 * n;q)) ≤ (r1/r(k)))
⊢ ∃q:unit-ball-approx(n;k * 8 * n). (↑isr(t approx-ball-to-ball(k * 8 * n;q)))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  f  :  B(n)  {}\mrightarrow{}  B(n)
3.  \mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x)
4.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
5.  r0  <  (e/r(3))
6.  t  :  \mforall{}p:B(n).  (((r(2)  *  e/r(3))  <  d(f  p;p))  \mvee{}  (d(f  p;p)  <  e))
7.  \mforall{}p:B(n).  ((\muparrow{}isr(t  p))  {}\mRightarrow{}  (d(f  p;p)  <  e))
8.  \mforall{}p:B(n).  ((\mneg{}\muparrow{}isr(t  p))  {}\mRightarrow{}  ((r(2)  *  e/r(3))  <  d(f  p;p)))
9.  del  :  \{del:\mBbbR{}|  r0  <  del\} 
10.  \mforall{}x,y:B(n).    ((d(x;y)  <  del)  {}\mRightarrow{}  (d(f  x;f  y)  <  (e/r(3))))
11.  k  :  \mBbbN{}\msupplus{}
12.  ((r1/r(k))  <  del)  \mwedge{}  ((r1/r(k))  <  (e/r(3)))
\mvdash{}  \mdownarrow{}\mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}isr(t  approx-ball-to-ball(k;q)))


By

---

Latex:
((InstLemma  `real-unit-ball-totally-bounded1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  D  0  With  \mkleeneopen{}k  *  8  *  n\mkleeneclose{} 
  THEN  Auto)

---

Home Index