---

Step * 1 1 1 1 1 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))
5. ¬(n = 0 ∈ ℤ)
6. e : {e:ℝ| r0 < e} 
7. d : ℕ+
8. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
9. x : B(n)
10. ∀y:B(n;r1). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
11. y : B(n)
12. d(x;y) < (r1/r(d))
13. d(f x;f y) ≤ (e/r(2))
⊢ d(f x;f y) < e
BY
{ ((RWO "-1" 0 THEN Auto) THEN nRMul ⌜r(2)⌝ 0⋅ THEN 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. e : {e:ℝ| r0 < e} 
7. d : ℕ+
8. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
9. x : B(n)
10. ∀y:B(n;r1). ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ (e/r(2))))
11. y : B(n)
12. d(x;y) < (r1/r(d))
13. d(f x;f y) ≤ (e/r(2))
⊢ e < (r(2) * 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))
5.  \mneg{}(n  =  0)
6.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
7.  d  :  \mBbbN{}\msupplus{}
8.  \mforall{}x,y:B(n;r1).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  (e/r(2))))
9.  x  :  B(n)
10.  \mforall{}y:B(n;r1).  ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  (e/r(2))))
11.  y  :  B(n)
12.  d(x;y)  <  (r1/r(d))
13.  d(f  x;f  y)  \mleq{}  (e/r(2))
\mvdash{}  d(f  x;f  y)  <  e


By

---

Latex:
((RWO  "-1"  0  THEN  Auto)  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index