---

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

∀n:ℕ. ∀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))} . ∀e:{e:ℝ| r0 < e} .
  ∃p:B(n). (↓d(f p;p) < e)
BY
{ (Auto
   THEN (CaseNat 0 `n'
         THENL [((RWO "real-vec-dist-dim0" 0 THENA Auto)
                 THEN InstLemma `real-unit-ball-0` []
                 THEN D 0 With ⌜⋅⌝ 
                 THEN Auto
                 THEN SubsumeC ⌜Top⌝⋅
                 THEN Auto)
               ; ((InstLemma `approx-fixpoint-unit-ball-0-ext` [⌜n⌝;⌜f⌝;⌜e⌝]⋅ THENA Auto)
                  THEN ExRepD
                  THEN (Assert ∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q))) BY
                              (D -1 THEN Unhide THEN Auto))
                  THEN Thin (-2)
                  THEN ExRepD
                  THEN FHyp (-4) [-1]
                  THEN Auto)]
        )
   ) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}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)))
                    \mwedge{}  (\mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x))\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    \mexists{}p:B(n).  (\mdownarrow{}d(f  p;p)  <  e)


By

---

Latex:
(Auto
  THEN  (CaseNat  0  `n'
              THENL  [((RWO  "real-vec-dist-dim0"  0  THENA  Auto)
                              THEN  InstLemma  `real-unit-ball-0`  []
                              THEN  D  0  With  \mkleeneopen{}\mcdot{}\mkleeneclose{} 
                              THEN  Auto
                              THEN  SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}
                              THEN  Auto)
                          ;  ((InstLemma  `approx-fixpoint-unit-ball-0-ext`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  ExRepD
                                THEN  (Assert  \mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}(t  approx-ball-to-ball(k;q)))  BY
                                                        (D  -1  THEN  Unhide  THEN  Auto))
                                THEN  Thin  (-2)
                                THEN  ExRepD
                                THEN  FHyp  (-4)  [-1]
                                THEN  Auto)]
            )
  )

---

Home Index