Step
*
1
1
2
of Lemma
unit-balls-homeomorphic+-2
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r B(n;r1)
4. B(n;r1) ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⊆r [r(-1), r1]^n
6. [r(-1), r1]^n ⊆r {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
7. f : FUN({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
8. g : FUN({q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
9. ∀x:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} . g (f x) ≡ x
10. ∀y:{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} . f (g y) ≡ y
11. B : ℕ+
12. ∀x1,x2:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} .
(mdist(max-metric(n);f x1;f x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
⊢ (∃g:FUN([r(-1), r1]^n ⟶ B(n;r1)). ((∀x:B(n;r1). g (f x) ≡ x) ∧ (∀y:[r(-1), r1]^n. f (g y) ≡ y)))
∧ (∃B:ℕ+. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f x1;f x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2))))
BY
{ D 0 }
1
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r B(n;r1)
4. B(n;r1) ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⊆r [r(-1), r1]^n
6. [r(-1), r1]^n ⊆r {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
7. f : FUN({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
8. g : FUN({q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
9. ∀x:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} . g (f x) ≡ x
10. ∀y:{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} . f (g y) ≡ y
11. B : ℕ+
12. ∀x1,x2:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} .
(mdist(max-metric(n);f x1;f x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
⊢ ∃g:FUN([r(-1), r1]^n ⟶ B(n;r1)). ((∀x:B(n;r1). g (f x) ≡ x) ∧ (∀y:[r(-1), r1]^n. f (g y) ≡ y))
2
1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⊆r B(n;r1)
4. B(n;r1) ⊆r {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}
5. {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⊆r [r(-1), r1]^n
6. [r(-1), r1]^n ⊆r {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}
7. f : FUN({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
8. g : FUN({q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
9. ∀x:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} . g (f x) ≡ x
10. ∀y:{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} . f (g y) ≡ y
11. B : ℕ+
12. ∀x1,x2:{q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} .
(mdist(max-metric(n);f x1;f x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
⊢ ∃B:ℕ+. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f x1;f x2) ≤ (r(B) * mdist(rn-metric(n);x1;x2)))
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 B(n;r1)
4. B(n;r1) \msubseteq{}r \{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
5. \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} \msubseteq{}r [r(-1), r1]\^{}n
6. [r(-1), r1]\^{}n \msubseteq{}r \{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\}
7. f : FUN(\{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\} \000C)
8. g : FUN(\{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\} \000C)
9. \mforall{}x:\{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} . g (f x) \mequiv{} x
10. \mforall{}y:\{q:\mBbbR{}\^{}n| mdist(max-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} . f (g y) \mequiv{} y
11. B : \mBbbN{}\msupplus{}
12. \mforall{}x1,x2:\{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} .
(mdist(max-metric(n);f x1;f x2) \mleq{} (r(B) * mdist(rn-metric(n);x1;x2)))
\mvdash{} (\mexists{}g:FUN([r(-1), r1]\^{}n {}\mrightarrow{} B(n;r1)). ((\mforall{}x:B(n;r1). g (f x) \mequiv{} x) \mwedge{} (\mforall{}y:[r(-1), r1]\^{}n. f (g y) \mequiv{} y)))
\mwedge{} (\mexists{}B:\mBbbN{}\msupplus{}. \mforall{}x1,x2:B(n;r1). (mdist(max-metric(n);f x1;f x2) \mleq{} (r(B) * mdist(rn-metric(n);x1;x2))))
By
Latex:
D 0
Home
Index