---

Step * of Lemma real-ball-uniform-continuity

∀k:ℕ. ∀n:ℕ+. ∀f:{f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1).  (req-vec(n;x;y) ⇒ req-vec(k;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))
BY
{ (Auto
   THEN (InstLemma `unit-balls-homeomorphic+-2` [⌜n⌝]⋅ THENA Auto)
   THEN D -1
   THEN ExRepD
   THEN (InstLemma `interval-cube-uniform-continuity` [⌜[r(-1), r1]⌝;⌜n⌝;⌜k⌝]⋅
         THENA (Auto THEN D 0 THEN Reduce 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))
⊢ ∃d:ℕ+. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d))) ⇒ (d(f x;f y) ≤ e))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}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))\}  .
\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    \mexists{}d:\mBbbN{}\msupplus{}.  \mforall{}x,y:B(n;r1).    ((d(x;y)  \mleq{}  (r1/r(d)))  {}\mRightarrow{}  (d(f  x;f  y)  \mleq{}  e))


By

---

Latex:
(Auto
  THEN  (InstLemma  `unit-balls-homeomorphic+-2`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  (InstLemma  `interval-cube-uniform-continuity`  [\mkleeneopen{}[r(-1),  r1]\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  0  THEN  Reduce  0  THEN  Auto)
              ))

---

Home Index