---

Step * of Lemma unit-balls-homeomorphic+

∀n:ℕ+. homeomorphic+({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ;rn-metric(n);{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} \000C;max-metric(n))
BY
{ ((Auto THEN (Assert λi.r0 ∈ ℝ^n BY Auto))
   THEN (Assert {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ≡ {p:ℝ^n| ||p|| ≤ r1}  BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN D -1
                THEN MemTypeCD
                THEN Auto
                THEN (Assert mdist(rn-metric(n);λi.r0;x) = ||x|| BY
                            ((RWO "mdist-symm" 0 THENA Auto) THEN RepUR ``mdist rn-metric`` 0 THEN Auto))
                THEN Auto))
   THEN D -1
   THEN (Assert ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p)) BY
               ((InstLemma `max-metric-leq-rn-metric` [⌜n⌝]⋅ THENA Auto)
                THEN (InstLemma `rn-metric-leq-max-metric` [⌜n⌝]⋅ THENA Auto)
                THEN (D 0 THENA Auto)
                THEN (D 6 With ⌜λi.r0⌝  THENA Auto)
                THEN (D -1 With ⌜p⌝  THENA Auto)
                THEN (D 5 With ⌜λi.r0⌝  THENA Auto)
                THEN (D -1 With ⌜p⌝  THENA Auto)
                THEN (Assert mdist(rn-metric(n);λi.r0;p) = ||p|| BY
                            (RepUR ``mdist rn-metric`` 0 THEN RWO "real-vec-dist-symmetry" 0 THEN Auto))
                THEN (RWO  "-1" 6 THENA Auto)
                THEN (RWO  "-1" 7 THENA Auto)
                THEN RepUR ``mdist scale-metric`` 6
                THEN Fold `mdist` 6
                THEN Auto
                THEN nRMul ⌜r(n)⌝ 0⋅
                THEN Auto))
   THEN (InstLemma `unit-ball-to-unit-cube` [⌜n⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (D 0 With ⌜g⌝  THENW (Auto THEN MemTypeCD THEN Auto THEN Thin (-1) THEN RepeatFor 3 (ParallelLast)))) }

1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ⊆r {p:ℝ^n| ||p|| ≤ r1} 
4. {p:ℝ^n| ||p|| ≤ r1}  ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} 
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. g : ℝ^n ⟶ ℝ^n
7. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
8. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
9. g ∈ {p:ℝ^n| ||p|| ≤ r1}  ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} 
10. g:FUN(ℝ^n;ℝ^n)
11. ∀x,y:{p:ℝ^n| ||p|| ≤ r1} .  (mdist(max-metric(n);g x;g y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))
⊢ (∃g@0:FUN({q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
    ((∀x:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} . g@0 (g x) ≡ x)
    ∧ (∀y:{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} . g (g@0 y) ≡ y)))
∧ (∃B:ℕ+
    ∀x1,x2:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} .
      (mdist(max-metric(n);g x1;g x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2))))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  homeomorphic+(\{q:\mBbbR{}\^{}n|  mdist(rn-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}  ;rn-metric(n);\{q:\mBbbR{}\^{}n|  mdist(max-metri\000Cc(n);\mlambda{}i.r0;q)  \mleq{}  r1\}  ;max-metric(n))


By

---

Latex:
((Auto  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n  BY  Auto))
  THEN  (Assert  \{q:\mBbbR{}\^{}n|  mdist(rn-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}    \mequiv{}  \{p:\mBbbR{}\^{}n|  ||p||  \mleq{}  r1\}    BY
                          (RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  (Assert  mdist(rn-metric(n);\mlambda{}i.r0;x)  =  ||x||  BY
                                                    ((RWO  "mdist-symm"  0  THENA  Auto)
                                                      THEN  RepUR  ``mdist  rn-metric``  0
                                                      THEN  Auto))
                            THEN  Auto))
  THEN  D  -1
  THEN  (Assert  \mforall{}p:\mBbbR{}\^{}n.  (r0  <  ||p||  \mLeftarrow{}{}\mRightarrow{}  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p))  BY
                          ((InstLemma  `max-metric-leq-rn-metric`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (InstLemma  `rn-metric-leq-max-metric`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (D  0  THENA  Auto)
                            THEN  (D  6  With  \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}    THENA  Auto)
                            THEN  (D  -1  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto)
                            THEN  (D  5  With  \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}    THENA  Auto)
                            THEN  (D  -1  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto)
                            THEN  (Assert  mdist(rn-metric(n);\mlambda{}i.r0;p)  =  ||p||  BY
                                                    (RepUR  ``mdist  rn-metric``  0
                                                      THEN  RWO  "real-vec-dist-symmetry"  0
                                                      THEN  Auto))
                            THEN  (RWO    "-1"  6  THENA  Auto)
                            THEN  (RWO    "-1"  7  THENA  Auto)
                            THEN  RepUR  ``mdist  scale-metric``  6
                            THEN  Fold  `mdist`  6
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto))
  THEN  (InstLemma  `unit-ball-to-unit-cube`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}g\mkleeneclose{} 
              THENW  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  Thin  (-1)  THEN  RepeatFor  3  (ParallelLast))
              ))

---

Home Index