---

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


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))
18. d(f x;f approx-ball-to-ball(k * 8 * n;q)) < (e/r(3))
⊢ r0 < d(f x;x)
BY
{ ((Assert d(x;approx-ball-to-ball(k * 8 * n;q)) < (e/r(3)) BY
          Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜approx-ball-to-ball(k * 8 * n;q) = y ∈ B(n)⌝⋅ THENA Auto)
   THEN ThinVars [`del';`q';`t']
   THEN Auto) }

1
1. n : ℕ+
2. f : B(n) ⟶ B(n)
3. e : {e:ℝ| r0 < e} 
4. r0 < (e/r(3))
5. k : ℕ+
6. (r1/r(k)) < (e/r(3))
7. x : B(n)
8. y : B(n)
9. (r(2) * e/r(3)) < d(f y;y)
10. d(f x;f y) < (e/r(3))
11. d(x;y) < (e/r(3))
⊢ r0 < d(f x;x)

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  d(x;approx-ball-to-ball(k  *  8  *  n;q))  <  (e/r(3))  BY
                Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}approx-ball-to-ball(k  *  8  *  n;q)  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVars  [`del';`q';`t']
  THEN  Auto)

---

Home Index