---

Step * 1 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
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)))
BY
{ (SupposeNot
   THEN D 3
   THEN Auto
   THEN UnfoldTopAb 0
   THEN (D -3 With ⌜x⌝  THENA Auto)
   THEN D -1
   THEN (InstHyp [⌜approx-ball-to-ball(k * 8 * n;q)⌝] 7⋅ THENA Auto)) }

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

---

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
13.  (r1/r(k))  <  (e/r(3))
14.  \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)))
\mvdash{}  \mexists{}q:unit-ball-approx(n;k  *  8  *  n).  (\muparrow{}isr(t  approx-ball-to-ball(k  *  8  *  n;q)))


By

---

Latex:
(SupposeNot
  THEN  D  3
  THEN  Auto
  THEN  UnfoldTopAb  0
  THEN  (D  -3  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}approx-ball-to-ball(k  *  8  *  n;q)\mkleeneclose{}]  7\mcdot{}  THENA  Auto))

---

Home Index