---

Step * 1 of Lemma unit-balls-homeomorphic+-2


1. n : ℕ+
2. λi.r0 ∈ ℝ^n
3. {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1}  ≡ B(n;r1)
4. {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ≡ [r(-1), r1]^n
⊢ homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]^n;max-metric(n))
BY
{ (D -2 THEN D -1 THEN (InstLemma `unit-balls-homeomorphic+` [⌜n⌝]⋅ THENA Auto)) }

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. 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))

---

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\}    \mequiv{}  B(n;r1)
4.  \{q:\mBbbR{}\^{}n|  mdist(max-metric(n);\mlambda{}i.r0;q)  \mleq{}  r1\}    \mequiv{}  [r(-1),  r1]\^{}n
\mvdash{}  homeomorphic+(B(n;r1);rn-metric(n);[r(-1),  r1]\^{}n;max-metric(n))


By

---

Latex:
(D  -2  THEN  D  -1  THEN  (InstLemma  `unit-balls-homeomorphic+`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index