---

Step * of Lemma find-approx-fp_wf

∀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} .
  (find-approx-fp(n;f;e) ∈ ∃p:B(n). (↓d(f p;p) < e))
BY
{ (Auto
   THEN (Subst' find-approx-fp(n;f;e) ~ TERMOF{approx-fixpoint-unit-ball-1-ext:o, \\v:l} n f e 0 THENA Computation)
   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\}  .
    (find-approx-fp(n;f;e)  \mmember{}  \mexists{}p:B(n).  (\mdownarrow{}d(f  p;p)  <  e))


By

---

Latex:
(Auto
  THEN  (Subst'  find-approx-fp(n;f;e)  \msim{}  TERMOF\{approx-fixpoint-unit-ball-1-ext:o,  \mbackslash{}\mbackslash{}v:l\}  n  f  e  0
              THENA  Computation
              )
  THEN  Auto)

---

Home Index