---

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

.....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))} 
BY
{ (Thin (-1) THEN D -1 THEN (MemTypeCD THENW Auto) THEN (Trivial ORELSE ParallelLast)) }

1
1. n : ℕ
2. f : B(n) ⟶ B(n)
3. ¬(∀x:B(n). f x ≠ x)
4. ∀x,y:B(n).  (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))
⊢ ∀e:{e:ℝ| r0 < e} . ∃del:{del:ℝ| r0 < del} . ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < e))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  n  :  \mBbbN{}
2.  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))\} 
3.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
\mvdash{}  f  \mmember{}  \{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))\000C)
              \mwedge{}  (\mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x))\} 


By

---

Latex:
(Thin  (-1)  THEN  D  -1  THEN  (MemTypeCD  THENW  Auto)  THEN  (Trivial  ORELSE  ParallelLast))

---

Home Index