---

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


1. n : ℕ+
2. f : {f:B(n) ⟶ B(n)| 
        (∀e:{e:ℝ| r0 < e} . ∃del:{del:ℝ| r0 < del} . ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < e)))
        ∧ (¬(∀x:B(n). f x ≠ x))} 
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)))
⊢ ↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑isr(t approx-ball-to-ball(k;q)))
BY
{ (D 2
   THEN ExRepD
   THEN (D 3 With ⌜(e/r(3))⌝  THENA Auto)
   THEN D -1
   THEN (Assert ∃k:ℕ+. (((r1/r(k)) < del) ∧ ((r1/r(k)) < (e/r(3)))) BY
               ((InstLemma `small-reciprocal-real` [⌜rmin(del;(e/r(3)))⌝]⋅
                 THENA (MemTypeCD THEN Auto THEN BLemma `rmin_strict_ub` THEN Auto)
                 )
               THENM (ParallelLast
                      THEN (Assert rmin(del;(e/r(3))) ≤ del BY
                                  Auto)
                      THEN (Assert rmin(del;(e/r(3))) ≤ (e/r(3)) BY
                                  Auto)
                      THEN Auto)
               ))
   THEN D -1) }

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) ∧ ((r1/r(k)) < (e/r(3)))
⊢ ↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑isr(t approx-ball-to-ball(k;q)))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  f  :  \{f:B(n)  {}\mrightarrow{}  B(n)| 
                (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}del:\{del:\mBbbR{}|  r0  <  del\}  .  \mforall{}x,y:B(n).    ((d(x;y)  <  del)  {}\mRightarrow{}  (d(f  x;f  y)  <  e)\000C))
                \mwedge{}  (\mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x))\} 
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)))
\mvdash{}  \mdownarrow{}\mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}isr(t  approx-ball-to-ball(k;q)))


By

---

Latex:
(D  2
  THEN  ExRepD
  THEN  (D  3  With  \mkleeneopen{}(e/r(3))\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  (Assert  \mexists{}k:\mBbbN{}\msupplus{}.  (((r1/r(k))  <  del)  \mwedge{}  ((r1/r(k))  <  (e/r(3))))  BY
                          ((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}rmin(del;(e/r(3)))\mkleeneclose{}]\mcdot{}
                              THENA  (MemTypeCD  THEN  Auto  THEN  BLemma  `rmin\_strict\_ub`  THEN  Auto)
                              )
                          THENM  (ParallelLast
                                        THEN  (Assert  rmin(del;(e/r(3)))  \mleq{}  del  BY
                                                                Auto)
                                        THEN  (Assert  rmin(del;(e/r(3)))  \mleq{}  (e/r(3))  BY
                                                                Auto)
                                        THEN  Auto)
                          ))
  THEN  D  -1)

---

Home Index