Step
*
1
1
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. homeomorphic+({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ;rn-metric(n);{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} ;max\000C-metric(n))
⊢ homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]^n;max-metric(n))
BY
{ (D -1 THEN ExRepD THEN D 0 With ⌜f⌝ ) }
1
.....wf.....
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)))
⊢ f ∈ FUN(B(n;r1) ⟶ [r(-1), r1]^n)
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))))
3
.....wf.....
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)))
13. f1 : FUN(B(n;r1) ⟶ [r(-1), r1]^n)
⊢ istype((∃g:FUN([r(-1), r1]^n ⟶ B(n;r1)). ((∀x:B(n;r1). g (f1 x) ≡ x) ∧ (∀y:[r(-1), r1]^n. f1 (g y) ≡ y)))
∧ (∃B:ℕ+. ∀x1,x2:B(n;r1). (mdist(max-metric(n);f1 x1;f1 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. homeomorphic+(\{q:\mBbbR{}\^{}n| mdist(rn-metric(n);\mlambda{}i.r0;q) \mleq{} r1\} ;rn-metric(n);\{q:\mBbbR{}\^{}n| mdist(max-metric(n)\000C;\mlambda{}i.r0;q) \mleq{} r1\} ;max-metric(n))
\mvdash{} homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]\^{}n;max-metric(n))
By
Latex:
(D -1 THEN ExRepD THEN D 0 With \mkleeneopen{}f\mkleeneclose{} )
Home
Index