---

Step * of Lemma approx-fixpoint-unit-ball-1-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} .
  ∃p:B(n). (↓d(f p;p) < e)
BY
{ Extract of Obid: approx-fixpoint-unit-ball-1
  not unfolding  isr real-vec-dist rlessw rinv rless-case int-to-real rmul rdiv unit-ball-ex-decider mu-ge divide 
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λn,f,e. if n=0
          then <Ax, Ax>
          else let k = mu-ge(λm.(unit-ball-ex-decider(m;n) 
                                 (λq.case 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 
                                                (λi.eval k = m in
                                                    λn.if (k) < (0)
                                                          then -((r(q i) (2 * n)) ÷ (-2) * k)
                                                          else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = m in
                                                                                              λn.if (k) < (0)
                                                                                                    then -((r(q i) 
                                                                                                            (2
                                                                                                            * n)) ÷ (-2)
                                                                                                         * k)
                                                                                                    else ((r(q i) 
                                                                                                           (2 * n)) ÷ 2
                                                                                                         * k))))
                                      of inl(x) =>
                                      inl x
                                      | inr(x) =>
                                      inr (λx.Ax) ));1) in
                   case unit-ball-ex-decider(k;n) 
                        (λq.case 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 
                                       (λi.eval k = k in
                                           λn.if (k) < (0)
                                                 then -((r(q i) (2 * n)) ÷ (-2) * k)
                                                 else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = k in
                                                                                     λn.if (k) < (0)
                                                                                           then -((r(q i) 
                                                                                                   (2 * n)) ÷ (-2) * k)
                                                                                           else ((r(q i) (2 * n)) ÷ 2
                                                                                                * k))))
                             of inl(x) =>
                             inl x
                             | inr(x) =>
                             inr (λx.Ax) )
                    of inl(x) =>
                    let q,%8 = x 
                    in <λi.eval k = k in
                           λn.if (k) < (0)  then -((r(q i) (2 * n)) ÷ (-2) * k)  else ((r(q i) (2 * n)) ÷ 2 * k)
                       , Ax
                       >
                    | inr(x) =>
                    let q,%8 = fix((λx.x)) 
                    in <λi.eval k = k in
                           λn.if (k) < (0)  then -((r(q i) (2 * n)) ÷ (-2) * k)  else ((r(q i) (2 * n)) ÷ 2 * k)
                       , Ax
                       > }

---

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:
...

---

Home Index