---

Step * 1 of Lemma unit-cube-to-unit-ball

.....assertion..... 
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
⊢ ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
BY
{ ((D 0 THENA Auto)
   THEN (D 3 With ⌜λi.r0⌝  THENA Auto)
   THEN (D -1 With ⌜p⌝  THENA Auto)
   THEN (D 2 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))) }

1
1. n : ℕ+
2. p : ℝ^n
3. mdist(rn-metric(n);λi.r0;p) ≤ mdist(r(n)*max-metric(n);λi.r0;p)
4. mdist(max-metric(n);λi.r0;p) ≤ mdist(rn-metric(n);λi.r0;p)
5. mdist(rn-metric(n);λi.r0;p) = ||p||
⊢ r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p)

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  max-metric(n)  \mleq{}  rn-metric(n)
3.  rn-metric(n)  \mleq{}  r(n)*max-metric(n)
\mvdash{}  \mforall{}p:\mBbbR{}\^{}n.  (r0  <  ||p||  \mLeftarrow{}{}\mRightarrow{}  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (D  3  With  \mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto)
  THEN  (D  2  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)))

---

Home Index