Step
*
2
2
2
3
of Lemma
unit-ball-to-unit-cube
.....wf.....
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. h ∈ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
12. g : ℝ^n ⟶ ℝ^n
⊢ istype((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))
∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p)
∧ (g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
∧ g:FUN(ℝ^n;ℝ^n)
∧ (∀x,y:{p:ℝ^n| ||p|| ≤ r1} . (mdist(max-metric(n);g x;g y) ≤ (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))))
BY
{ (Reduce 0 THEN (D 0 THENL [Auto; (D 0 THENL [(D 0 THENL [Auto; (DVar `p' THEN Auto)]); Auto])])) }
1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. max-metric(n) ≤ rn-metric(n)
4. rn-metric(n) ≤ r(n)*max-metric(n)
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . ((||p||/mdist(max-metric(n);p;λi.r0))*p ∈ ℝ^n)
7. h : ℝ^n ⟶ ℝ^n
8. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
9. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . h p ≡ (||p||/mdist(max-metric(n);p;λi.r0))*p
10. λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n) ⇒ h:FUN(ℝ^n;ℝ^n)
11. h ∈ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
12. g : ℝ^n ⟶ ℝ^n
13. x : ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
14. p : ℝ^n
15. r0 < mdist(max-metric(n);λi.r0;p)
⊢ mdist(max-metric(n);p;λi.r0) ≠ r0
Latex:
Latex:
.....wf.....
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:\mBbbR{}\^{}n. (r0 < ||p|| \mLeftarrow{}{}\mRightarrow{} r0 < mdist(max-metric(n);\mlambda{}i.r0;p))
6. \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)
7. h : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
8. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} h p \mequiv{} \mlambda{}i.r0)
9. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);p;\mlambda{}i.r0)\} . h p \mequiv{} (||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p
10. \mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p:FUN(\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);p;\mlambda{}i.r0)\} ;\mBbbR{}\^{}n) {}\000C\mRightarrow{} h:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
11. h \mmember{} \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
12. g : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
\mvdash{} istype((\mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} g p \mequiv{} \mlambda{}i.r0))
\mwedge{} (\mforall{}p:\{p:\mBbbR{}\^{}n| r0 < mdist(max-metric(n);\mlambda{}i.r0;p)\}
g p \mequiv{} (\mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p) p)
\mwedge{} (g \mmember{} \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} )
\mwedge{} g:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
\mwedge{} (\mforall{}x,y:\{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} .
(mdist(max-metric(n);g x;g y) \mleq{} (r((2 * n) + 1) * mdist(rn-metric(n);x;y)))))
By
Latex:
(Reduce 0 THEN (D 0 THENL [Auto; (D 0 THENL [(D 0 THENL [Auto; (DVar `p' THEN Auto)]); Auto])]))
Home
Index