---

Step * 1 1 2 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)))
⊢ ∃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 With ⌜B⌝  THENW 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. 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)))
⊢ ∀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{}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  With  \mkleeneopen{}B\mkleeneclose{}    THENW  Auto)

---

Home Index