---

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

∀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} .
  ∃t:B(n) ⟶ 𝔹
   ((∀p:B(n). ((↑(t p)) ⇒ (↓d(f p;p) < e))) ∧ (↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q)))))
BY
{ Extract of Obid: approx-fixpoint-unit-ball-0
  not unfolding  isr real-vec-dist rlessw rinv rless-case int-to-real rmul rdiv
  finishing with Auto
  normalizes to:
  
  λn,f,e. <λp.isr(rless-case((r(2) * e/r(3));e;(((rlessw(((r(2) * e/r(3)) * r(3)) * rinv(r(3));(e * r(3)) * rinv(r(3)))
              * 20)
              + 1)
              * 20)
              + 1;d(f p;p)))
          , λ_,_. Ax
          , Ax> }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \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{}t:B(n)  {}\mrightarrow{}  \mBbbB{}
      ((\mforall{}p:B(n).  ((\muparrow{}(t  p))  {}\mRightarrow{}  (\mdownarrow{}d(f  p;p)  <  e)))
      \mwedge{}  (\mdownarrow{}\mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}(t  approx-ball-to-ball(k;q)))))


By

---

Latex:
Extract  of  Obid:  approx-fixpoint-unit-ball-0
not  unfolding    isr  real-vec-dist  rlessw  rinv  rless-case  int-to-real  rmul  rdiv
finishing  with  Auto
normalizes  to:

\mlambda{}n,f,e.  <\mlambda{}p.isr(rless-case((r(2)  *  e/r(3));e;(((rlessw(((r(2)  *  e/r(3))  *  r(3))  *  rinv(r(3));(e
                        *  r(3))
                        *  rinv(r(3)))
                        *  20)
                        +  1)
                        *  20)
                        +  1;d(f  p;p)))
                ,  \mlambda{}$_{}$,$_{}$.  Ax
                ,  Ax>

---

Home Index