---

Step * of Lemma unit-balls-homeomorphic+-2

∀n:ℕ+. homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]^n;max-metric(n))
BY
{ (Auto
   THEN (Assert λi.r0 ∈ ℝ^n BY
               Auto)
   THEN (Assert {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ≡ B(n;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 (Assert {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ≡ [r(-1), r1]^n BY
               (RepeatFor 2 ((D 0 THENA Auto))
                THEN D -1
                THEN MemTypeCD
                THEN Auto
                THEN (RWO "max-metric-mdist-from-zero-2" (-2) ORELSE RWO "max-metric-mdist-from-zero-2" 0)
                THEN Auto
                THEN D -2 With ⌜i⌝ 
                THEN All Reduce
                THEN Auto))) }

1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ≡ B(n;r1)
4. {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ≡ [r(-1), r1]^n
⊢ homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]^n;max-metric(n))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  homeomorphic+(B(n;r1);rn-metric(n);[r(-1),  r1]\^{}n;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{}  B(n;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  (Assert  \{q:\mBbbR{}\^{}n|  mdist(max-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}    \mequiv{}  [r(-1),  r1]\^{}n  BY
                          (RepeatFor  2  ((D  0  THENA  Auto))
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  (RWO  "max-metric-mdist-from-zero-2"  (-2)
                            ORELSE  RWO  "max-metric-mdist-from-zero-2"  0
                            )
                            THEN  Auto
                            THEN  D  -2  With  \mkleeneopen{}i\mkleeneclose{} 
                            THEN  All  Reduce
                            THEN  Auto)))

---

Home Index