Step
*
1
1
2
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. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
14. h:FUN(ℝ^n;ℝ^n)
15. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
16. r0 < ||y||
17. h y ≡ (mdist(max-metric(n);λi.r0;y)/||y||)*y
⊢ g (h y) ≡ y
BY
{ ((Assert λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} BY
(MemTypeCD THEN Auto THEN RWO "mdist-same" 0 THEN Auto))
THEN (D 8 With ⌜(mdist(max-metric(n);λi.r0;y)/||y||)*y⌝ THENA (MemTypeCD THEN Auto))
) }
1
.....set predicate.....
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. g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
9. g:FUN(ℝ^n;ℝ^n)
10. h : ℝ^n ⟶ ℝ^n
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
13. h:FUN(ℝ^n;ℝ^n)
14. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
15. r0 < ||y||
16. h y ≡ (mdist(max-metric(n);λi.r0;y)/||y||)*y
17. λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
⊢ r0 < mdist(max-metric(n);λi.r0;(mdist(max-metric(n);λi.r0;y)/||y||)*y)
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. g ∈ {p:ℝ^n| ||p|| ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
9. g:FUN(ℝ^n;ℝ^n)
10. h : ℝ^n ⟶ ℝ^n
11. ∀p:ℝ^n. (req-vec(n;p;λi.r0) ⇒ h p ≡ λi.r0)
12. h ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
13. h:FUN(ℝ^n;ℝ^n)
14. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
15. r0 < ||y||
16. h y ≡ (mdist(max-metric(n);λi.r0;y)/||y||)*y
17. λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
18. g (mdist(max-metric(n);λi.r0;y)/||y||)*y ≡ (λp.(||p||/mdist(max-metric(n);p;λi.r0))*p)
(mdist(max-metric(n);λi.r0;y)/||y||)*y
⊢ g (h y) ≡ y
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. 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\}
14. h:FUN(\mBbbR{}\^{}n;\mBbbR{}\^{}n)
15. y : \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
16. r0 < ||y||
17. h y \mequiv{} (mdist(max-metric(n);\mlambda{}i.r0;y)/||y||)*y
\mvdash{} g (h y) \mequiv{} y
By
Latex:
((Assert \mlambda{}i.r0 \mmember{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} BY
(MemTypeCD THEN Auto THEN RWO "mdist-same" 0 THEN Auto))
THEN (D 8 With \mkleeneopen{}(mdist(max-metric(n);\mlambda{}i.r0;y)/||y||)*y\mkleeneclose{} THENA (MemTypeCD THEN Auto))
)
Home
Index