---

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

.....rewrite subgoal..... 
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
6. m : ℕ+
7. p : ℝ^n
8. r0 < mdist(max-metric(n);p;λi.r0)
9. mdist(max-metric(n);p;λi.r0) ≤ (r(4)/r(m))
10. r0 < mdist(max-metric(n);λi.r0;p)
11. r0 < ||p||
12. (||p||/mdist(max-metric(n);p;λi.r0)) ∈ ℝ
13. v : ℝ
14. mdist(max-metric(n);p;λi.r0) = v ∈ ℝ
15. r0 < v
16. r0 < mdist(max-metric(n);λi.r0;p)
⊢ r0 ≤ (||p||/v)
BY
{ (nRMul ⌜v⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
.....rewrite  subgoal..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n
3.  max-metric(n)  \mleq{}  rn-metric(n)
4.  rn-metric(n)  \mleq{}  r(n)*max-metric(n)
5.  \mforall{}p:\{p:\mBbbR{}\^{}n|  r0  <  mdist(max-metric(n);p;\mlambda{}i.r0)\}  .  ((||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p  \mmember{}  \mBbbR{}\^{}n)
6.  m  :  \mBbbN{}\msupplus{}
7.  p  :  \mBbbR{}\^{}n
8.  r0  <  mdist(max-metric(n);p;\mlambda{}i.r0)
9.  mdist(max-metric(n);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(m))
10.  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p)
11.  r0  <  ||p||
12.  (||p||/mdist(max-metric(n);p;\mlambda{}i.r0))  \mmember{}  \mBbbR{}
13.  v  :  \mBbbR{}
14.  mdist(max-metric(n);p;\mlambda{}i.r0)  =  v
15.  r0  <  v
16.  r0  <  mdist(max-metric(n);\mlambda{}i.r0;p)
\mvdash{}  r0  \mleq{}  (||p||/v)


By

---

Latex:
(nRMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index