---

Step * 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))
⊢ r0 < d(f x;x)
BY
{ (Assert d(f x;f approx-ball-to-ball(k * 8 * n;q)) < (e/r(3)) BY
         (BackThruSomeHyp THEN 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))
18. d(f x;f approx-ball-to-ball(k * 8 * n;q)) < (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))
\mvdash{}  r0  <  d(f  x;x)


By

---

Latex:
(Assert  d(f  x;f  approx-ball-to-ball(k  *  8  *  n;q))  <  (e/r(3))  BY
              (BackThruSomeHyp  THEN  Auto))

---

Home Index