---

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

∀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
{ (Intros THEN UseWitness ⌜find-approx-fp(n;f;e)⌝⋅ 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:
(Intros  THEN  UseWitness  \mkleeneopen{}find-approx-fp(n;f;e)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index