Step
*
1
1
1
of Lemma
unit-balls-homeomorphic+
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r {p:ℝ^n| ||p|| ≤ r1}
4. {p:ℝ^n| ||p|| ≤ r1} ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. g : ℝ^n ⟶ ℝ^n
7. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
8. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
9. g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
10. g:FUN(ℝ^n;ℝ^n)
11. h : ℝ^n ⟶ ℝ^n
12. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
13. ∀p:{p:ℝ^n| r0 < ||p||} . h p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
14. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
15. h:FUN(ℝ^n;ℝ^n)
16. x : {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
⊢ h (g x) ≡ x
BY
{ (StableCases ⌜r0 < ||x||⌝⋅ THEN Try (Complete (Auto))) }
1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r {p:ℝ^n| ||p|| ≤ r1}
4. {p:ℝ^n| ||p|| ≤ r1} ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. g : ℝ^n ⟶ ℝ^n
7. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
8. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
9. g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
10. g:FUN(ℝ^n;ℝ^n)
11. h : ℝ^n ⟶ ℝ^n
12. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
13. ∀p:{p:ℝ^n| r0 < ||p||} . h p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
14. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
15. h:FUN(ℝ^n;ℝ^n)
16. x : {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
17. r0 < ||x||
⊢ h (g x) ≡ x
2
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r {p:ℝ^n| ||p|| ≤ r1}
4. {p:ℝ^n| ||p|| ≤ r1} ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. ∀p:ℝ^n. (r0 < ||p|| ⇐⇒ r0 < mdist(max-metric(n);λi.r0;p))
6. g : ℝ^n ⟶ ℝ^n
7. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ g p ≡ λi.r0)
8. ∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g p ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p) p
9. g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
10. g:FUN(ℝ^n;ℝ^n)
11. h : ℝ^n ⟶ ℝ^n
12. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
13. ∀p:{p:ℝ^n| r0 < ||p||} . h p ≡ (λp.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p
14. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
15. h:FUN(ℝ^n;ℝ^n)
16. x : {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
17. ¬(r0 < ||x||)
⊢ h (g x) ≡ x
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. \mlambda{}i.r0 \mmember{} \mBbbR{}\^{}n
3. \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} \msubseteq{}r \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\}
4. \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} \msubseteq{}r \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
5. \mforall{}p:\mBbbR{}\^{}n. (r0 < ||p|| \mLeftarrow{}{}\mRightarrow{} r0 < mdist(max-metric(n);\mlambda{}i.r0;p))
6. g : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
7. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} g p \mequiv{} \mlambda{}i.r0)
8. \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
9. g \mmember{} \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\} {}\mrightarrow{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
10. g:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
11. h : \mBbbR{}\^{}n {}\mrightarrow{} \mBbbR{}\^{}n
12. \mforall{}p:\mBbbR{}\^{}n. (req-vec(n;p;\mlambda{}i.r0) {}\mRightarrow{} h p \mequiv{} \mlambda{}i.r0)
13. \mforall{}p:\{p:\mBbbR{}\^{}n| r0 < ||p||\} . h p \mequiv{} (\mlambda{}p.(mdist(max-metric(n);\mlambda{}i.r0;p)/||p||)*p) p
14. h \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\}
15. h:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
16. x : \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
\mvdash{} h (g x) \mequiv{} x
By
Latex:
(StableCases \mkleeneopen{}r0 < ||x||\mkleeneclose{}\mcdot{} THEN Try (Complete (Auto)))
Home
Index