---

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

∀n:ℕ. ∀f:{f:B(n) ⟶ B(n)| (∀x,y:B(n).  (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))) ∧ (¬(∀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 MemCD THEN Try (QuickAuto)) }

1
.....subterm..... T:t
2:n
1. n : ℕ
2. f : {f:B(n) ⟶ B(n)| (∀x,y:B(n).  (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))) ∧ (¬(∀x:B(n). f x ≠ x))} 
3. e : {e:ℝ| r0 < e} 
⊢ 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))} 

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\{f:B(n)  {}\mrightarrow{}  B(n)| 
                    (\mforall{}x,y:B(n).    (req-vec(n;x;y)  {}\mRightarrow{}  req-vec(n;f  x;f  y)))  \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  MemCD  THEN  Try  (QuickAuto))

---

Home Index