Proof of Nuprl Lemma : unit-ball-to-unit-cube

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

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. ∃g:ℝ^n ⟶ ℝ^n
(((∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0))

    ∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p))

    ∧ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p:FUN({p:ℝ^n| r0 < mdist(max-metric(n);p;λi.r0)} ;ℝ^n)

⇒ g:FUN(ℝ^n;ℝ^n))\000C)
⊢ ∃g:ℝ^n ⟶ ℝ^n
((∀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 -1
THEN ExRepD
THEN RenameVar `h' (-4)

   THEN Assert ⌜h ∈ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⌝⋅) }

1
.....assertion.....
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)

⊢ h ∈ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}

2
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}

⊢ ∃g:ℝ^n ⟶ ℝ^n
((∀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)))))

Latex:

Latex:
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. \mexists{}g:\mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n (((\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);p;\mlambda{}i.r0)\} g p \mequiv{} (\mlambda{}p.(||p||/mdist(max-metric(n);p;\mlambda{}i.r0))*p) p)) \mwedge{} (\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{} g:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n))) \mvdash{} \mexists{}g:\mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n ((\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 -1 THEN ExRepD THEN RenameVar `h' (-4) THEN Assert \mkleeneopen{}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\} \mkleeneclose{}\mcdot{}) Home Index