Step
*
1
1
2
2
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. ∀x1,x2:ℝ^n. (x1 ≡ x2 ⇒ g x1 ≡ g x2)
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. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
17. ¬(r0 < ||y||)
18. ||y|| ≤ r0
19. ||y|| = r0
20. req-vec(n;y;λi.r0)
21. h y ≡ λi.r0
22. λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
23. h (λi.r0) ≡ λi.r0
24. λi.r0 ∈ {p:ℝ^n| ||p|| ≤ r1}
25. g (h y) ≡ g (λi.r0)
⊢ g (λi.r0) ≡ y
BY
{ ((Assert req-vec(n;λi.r0;y) BY EAuto 1) THEN RWO "7" 0 THEN Auto) }
1
.....rewrite subgoal.....
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. ∀x1,x2:ℝ^n. (x1 ≡ x2 ⇒ g x1 ≡ g x2)
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. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
17. ¬(r0 < ||y||)
18. ||y|| ≤ r0
19. ||y|| = r0
20. req-vec(n;y;λi.r0)
21. h y ≡ λi.r0
22. λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
23. h (λi.r0) ≡ λi.r0
24. λi.r0 ∈ {p:ℝ^n| ||p|| ≤ r1}
25. g (h y) ≡ g (λi.r0)
26. req-vec(n;λi.r0;y)
⊢ req-vec(n;λi.r0;λi.r0)
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. ∀x1,x2:ℝ^n. (x1 ≡ x2 ⇒ g x1 ≡ g x2)
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. y : {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
17. ¬(r0 < ||y||)
18. ||y|| ≤ r0
19. ||y|| = r0
20. req-vec(n;y;λi.r0)
21. h y ≡ λi.r0
22. λi.r0 ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
23. h (λi.r0) ≡ λi.r0
24. λi.r0 ∈ {p:ℝ^n| ||p|| ≤ r1}
25. g (h y) ≡ g (λi.r0)
26. req-vec(n;λi.r0;y)
⊢ λi.r0 ≡ 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. \mforall{}x1,x2:\mBbbR{}\^{}n. (x1 \mequiv{} x2 {}\mRightarrow{} g x1 \mequiv{} g x2)
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. y : \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
17. \mneg{}(r0 < ||y||)
18. ||y|| \mleq{} r0
19. ||y|| = r0
20. req-vec(n;y;\mlambda{}i.r0)
21. h y \mequiv{} \mlambda{}i.r0
22. \mlambda{}i.r0 \mmember{} \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
23. h (\mlambda{}i.r0) \mequiv{} \mlambda{}i.r0
24. \mlambda{}i.r0 \mmember{} \{p:\mBbbR{}\^{}n| ||p|| \mleq{} r1\}
25. g (h y) \mequiv{} g (\mlambda{}i.r0)
\mvdash{} g (\mlambda{}i.r0) \mequiv{} y
By
Latex:
((Assert req-vec(n;\mlambda{}i.r0;y) BY EAuto 1) THEN RWO "7" 0 THEN Auto)
Home
Index