---

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


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))
BY
{ (CaseNat 0 `n'
   THENL [((Auto THEN D 0 With ⌜r1⌝ ) THEN Auto THEN RWO "real-vec-dist-dim0" 0 THEN Auto)
         ; (InstLemma `real-ball-uniform-continuity` [⌜n⌝;⌜n⌝]⋅ THENA Auto)]
) }

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))
5. ¬(n = 0 ∈ ℤ)
6. ∀f:{f:B(n;r1) ⟶ ℝ^n| ∀x,y:B(n;r1).  (req-vec(n;x;y) ⇒ req-vec(n;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
     ∃d:ℕ+. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
⊢ ∀e:{e:ℝ| r0 < e} . ∃del:{del:ℝ| r0 < del} . ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < e))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  B(n)  {}\mrightarrow{}  B(n)
3.  \mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x)
4.  \mforall{}x,y:B(n).    (req-vec(n;x;y)  {}\mRightarrow{}  req-vec(n;f  x;f  y))
\mvdash{}  \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))


By

---

Latex:
(CaseNat  0  `n'
  THENL  [((Auto  THEN  D  0  With  \mkleeneopen{}r1\mkleeneclose{}  )  THEN  Auto  THEN  RWO  "real-vec-dist-dim0"  0  THEN  Auto)
              ;  (InstLemma  `real-ball-uniform-continuity`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)]
)

---

Home Index