Step
*
2
2
1
2
1
1
1
1
of Lemma
unit-cube-to-unit-ball
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
5. ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n)
6. λi.r0 ∈ ℝ^n
7. g : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (mdist(max-metric(n);λi.r0;p)/||p||)*p
10. g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
13. x1 : {p:ℝ^n| r0 < ||p||}
14. x2 : {p:ℝ^n| r0 < ||p||}
15. x1 ≡ x2
16. req-vec(n;x1;x2)
⊢ (mdist(max-metric(n);λi.r0;x1)/||x1||)*x1 ≡ (mdist(max-metric(n);λi.r0;x2)/||x2||)*x2
BY
{ (Assert req-vec(n;(mdist(max-metric(n);λi.r0;x1)/||x1||)*x1;(mdist(max-metric(n);λi.r0;x2)/||x2||)*x2) BY
(DVar `x1' THEN DVar `x2' THEN RWO "-1" 0 THEN Auto)) }
1
.....aux.....
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
5. ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n)
6. λi.r0 ∈ ℝ^n
7. g : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (mdist(max-metric(n);λi.r0;p)/||p||)*p
10. g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
13. x1 : ℝ^n
14. r0 < ||x1||
15. x2 : ℝ^n
16. r0 < ||x2||
17. x1 ≡ x2
18. req-vec(n;x1;x2)
⊢ req-vec(n;(mdist(max-metric(n);λi.r0;x1)/||x2||)*x2;(mdist(max-metric(n);λi.r0;x2)/||x2||)*x2)
2
1. n : ℕ+
2. max-metric(n) ≤ rn-metric(n)
3. rn-metric(n) ≤ r(n)*max-metric(n)
4. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
5. ∀p:{p:ℝ^n| r0 < ||p||} . ((mdist(max-metric(n);λi.r0;p)/||p||)*p ∈ ℝ^n)
6. λi.r0 ∈ ℝ^n
7. g : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (mdist(max-metric(n);λi.r0;p)/||p||)*p
10. g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
12. ∀p:{p:ℝ^n| r0 < ||p||} . g p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
13. x1 : {p:ℝ^n| r0 < ||p||}
14. x2 : {p:ℝ^n| r0 < ||p||}
15. x1 ≡ x2
16. req-vec(n;x1;x2)
17. req-vec(n;(mdist(max-metric(n);λi.r0;x1)/||x1||)*x1;(mdist(max-metric(n);λi.r0;x2)/||x2||)*x2)
⊢ (mdist(max-metric(n);λi.r0;x1)/||x1||)*x1 ≡ (mdist(max-metric(n);λi.r0;x2)/||x2||)*x2
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. max-metric(n) \mleq{} rn-metric(n)
3. rn-metric(n) \mleq{} r(n)*max-metric(n)
4. \mforall{}p:\mBbbR{}\^{}n. (r0 < ||p|| \mLeftarrow{}{}\mRightarrow{} r0 < mdist(max-metric(n);\mlambda{}i.r0;p))
5. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < ||p||\} . ((mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p \mmember{} \mBbbR{}\^{}n)
6. \mlambda{}i.r0 \mmember{} \mBbbR{}\^{}n
7. g : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
8. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} g p \mequiv{} \mlambda{}i.r0)
9. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < ||p||\} . g p \mequiv{} (mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p
10. g \mmember{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
11. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} g p \mequiv{} \mlambda{}i.r0)
12. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < ||p||\} . g p \mequiv{} (\mlambda{}p.(mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p) p
13. x1 : \{p:\mBbbR{}\^{}n| r0 < ||p||\}
14. x2 : \{p:\mBbbR{}\^{}n| r0 < ||p||\}
15. x1 \mequiv{} x2
16. req-vec(n;x1;x2)
\mvdash{} (mdist(max-metric(n);\mlambda{}i.r0;x1)/||x1||)*x1 \mequiv{} (mdist(max-metric(n);\mlambda{}i.r0;x2)/||x2||)*x2
By
Latex:
(Assert req-vec(n;(mdist(max-metric(n);\mlambda{}i.r0;x1)/||x1||)*x1;(mdist(max-metric(n);...;x2)/...)*x2) BY
(DVar `x1' THEN DVar `x2' THEN RWO "-1" 0 THEN Auto))
Home
Index