Step
*
1
1
2
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. 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
⊢ ∃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))
BY
{ D 0 With ⌜g⌝ }
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
⊢ g ∈ FUN([r(-1), r1]^n ⟶ B(n;r1))
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
⊢ (∀x:B(n;r1). g (f x) ≡ x) ∧ (∀y:[r(-1), r1]^n. f (g y) ≡ y)
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. g1 : FUN([r(-1), r1]^n ⟶ B(n;r1))
⊢ istype((∀x:B(n;r1). g1 (f x) ≡ x) ∧ (∀y:[r(-1), r1]^n. f (g1 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 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
\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))
By
Latex:
D 0 With \mkleeneopen{}g\mkleeneclose{}
Home
Index