---

Step * 1 1 1 of Lemma real-ball-uniform-continuity

.....assertion..... 
1. k : ℕ
2. n : ℕ+
3. f : {f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1).  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} 
4. e : {e:ℝ| r0 < e} 
5. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
6. g : FUN([r(-1), r1]^n ⟶ B(n;r1))
7. ∀x:B(n;r1). g (f1 x) ≡ x
8. ∀y:[r(-1), r1]^n. f1 (g y) ≡ y
9. B : ℕ+
10. ∀x1,x2:B(n;r1).  (mdist(max-metric(n);f1 x1;f1 x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
11. ∀f:{f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n.  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
      ∃d:ℕ+. ∀x,y:[r(-1), r1]^n.  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
12. f o g ∈ {f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n.  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} 
13. d : ℕ+
14. ∀x,y:[r(-1), r1]^n.  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f (g x);f (g y)) ≤ e))
⊢ ∃d2:ℕ+. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d2))) ⇒ (d(f1 x;f1 y) ≤ (r1/r(d))))
BY
{ (D 0 With ⌜B * d * n⌝ 
   THEN Auto
   THEN (InstHyp [⌜x⌝;⌜y⌝] 10⋅ THENA Auto)
   THEN (Subst' mdist(rn-metric(n);x;y) ~ d(x;y) -1 THENA (RepUR ``mdist rn-metric`` 0 THEN Auto))) }

1
1. k : ℕ
2. n : ℕ+
3. f : {f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1).  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} 
4. e : {e:ℝ| r0 < e} 
5. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
6. g : FUN([r(-1), r1]^n ⟶ B(n;r1))
7. ∀x:B(n;r1). g (f1 x) ≡ x
8. ∀y:[r(-1), r1]^n. f1 (g y) ≡ y
9. B : ℕ+
10. ∀x1,x2:B(n;r1).  (mdist(max-metric(n);f1 x1;f1 x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
11. ∀f:{f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n.  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} . ∀e:{e:ℝ| r0 < e} .
      ∃d:ℕ+. ∀x,y:[r(-1), r1]^n.  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))
12. f o g ∈ {f:[r(-1), r1]^n ⟶ ℝ^k| ∀x,y:[r(-1), r1]^n.  (req-vec(n;x;y) ⇒ req-vec(k;f x;f y))} 
13. d : ℕ+
14. ∀x,y:[r(-1), r1]^n.  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f (g x);f (g y)) ≤ e))
15. x : B(n;r1)
16. y : B(n;r1)
17. d(x;y) ≤ (r1/r(B * d * n))
18. mdist(max-metric(n);f1 x;f1 y) ≤ (r(B) * d(x;y))
⊢ d(f1 x;f1 y) ≤ (r1/r(d))

---

Latex:

---

Latex:
.....assertion..... 
1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}\msupplus{}
3.  f  :  \{f:B(n;r1)  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:B(n;r1).    (req-vec(n;x;y)  {}\mRightarrow{}  req-vec(k;f  x;f  y))\} 
4.  e  :  \{e:\mBbbR{}|  r0  <  e\} 
5.  f1  :  FUN(B(n;r1)  {}\mrightarrow{}  [r(-1),  r1]\^{}n)
6.  g  :  FUN([r(-1),  r1]\^{}n  {}\mrightarrow{}  B(n;r1))
7.  \mforall{}x:B(n;r1).  g  (f1  x)  \mequiv{}  x
8.  \mforall{}y:[r(-1),  r1]\^{}n.  f1  (g  y)  \mequiv{}  y
9.  B  :  \mBbbN{}\msupplus{}
10.  \mforall{}x1,x2:B(n;r1).    (mdist(max-metric(n);f1  x1;f1  x2)  \mleq{}  (r(B)  *  mdist(rn-metric(n);x1;x2)))
11.  \mforall{}f:\{f:[r(-1),  r1]\^{}n  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:[r(-1),  r1]\^{}n.    (req-vec(n;x;y)  {}\mRightarrow{}  req-vec(k;f  x;f  y))\}  .
        \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
            \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}x,y:[r(-1),  r1]\^{}n.    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))
12.  f  o  g  \mmember{}  \{f:[r(-1),  r1]\^{}n  {}\mrightarrow{}  \mBbbR{}\^{}k|  \mforall{}x,y:[r(-1),  r1]\^{}n.    (req-vec(n;x;y)  {}\mRightarrow{}  req-vec(k;f  x;f  y))\} 
13.  d  :  \mBbbN{}\msupplus{}
14.  \mforall{}x,y:[r(-1),  r1]\^{}n.    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  (g  x);f  (g  y))  \mleq{}  e))
\mvdash{}  \mexists{}d2:\mBbbN{}\msupplus{}.  \mforall{}x,y:B(n;r1).    ((d(x;y)  \mleq{}  (r1/r(d2)))  {}\mRightarrow{}  (d(f1  x;f1  y)  \mleq{}  (r1/r(d))))


By

---

Latex:
(D  0  With  \mkleeneopen{}B  *  d  *  n\mkleeneclose{} 
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  10\mcdot{}  THENA  Auto)
  THEN  (Subst'  mdist(rn-metric(n);x;y)  \msim{}  d(x;y)  -1  THENA  (RepUR  ``mdist  rn-metric``  0  THEN  Auto)))

---

Home Index