---

Step * 1 1 of Lemma compact-metric-to-metric-continuity


1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
9. k : ℕ+
10. m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
⊢ ∃delta:{d:ℝ| r0 < d} . ∀x,y:X.  ((mdist(d;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k))))
BY
{ ((RenameVar `cmp2' (-1) THEN RenameVar `mtb2' (-2))
   THEN (InstLemma `compact-metric-to-real-continuity` [⌜i:ℕ2 ⟶ X⌝;⌜prod-metric(2;λi.d)⌝;⌜<cmp2, mtb2>⌝;
         ⌜λp.mdist(dY;f (p 0);f (p 1))⌝]⋅
         THENA (Auto THEN MemTypeCD THEN Auto THEN RepUR ``is-mfun so_apply`` 0 THEN Auto)
         )
   ) }

1
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
9. k : ℕ+
10. mtb2 : m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. cmp2 : mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
12. x1 : i:ℕ2 ⟶ X
13. x2 : i:ℕ2 ⟶ X
14. x1 ≡ x2
⊢ mdist(dY;f (x1 0);f (x1 1)) ≡ mdist(dY;f (x2 0);f (x2 1))

2
1. X : Type
2. d : metric(X)
3. cmplt : mcomplete(X with d)
4. mtb : m-TB(X;d)
5. Y : Type
6. dY : metric(Y)
7. f : X ⟶ Y
8. ∀x,y:X.  (x ≡ y ⇒ f x ≡ f y)
9. k : ℕ+
10. mtb2 : m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. cmp2 : mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
12. UC(λp.mdist(dY;f (p 0);f (p 1)):i:ℕ2 ⟶ X ⟶ ℝ)
⊢ ∃delta:{d:ℝ| r0 < d} . ∀x,y:X.  ((mdist(d;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k))))

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  cmplt  :  mcomplete(X  with  d)
4.  mtb  :  m-TB(X;d)
5.  Y  :  Type
6.  dY  :  metric(Y)
7.  f  :  X  {}\mrightarrow{}  Y
8.  \mforall{}x,y:X.    (x  \mequiv{}  y  {}\mRightarrow{}  f  x  \mequiv{}  f  y)
9.  k  :  \mBbbN{}\msupplus{}
10.  m-TB(i:\mBbbN{}2  {}\mrightarrow{}  X;prod-metric(2;\mlambda{}\msubtwo{}i.d))
11.  mcomplete(i:\mBbbN{}2  {}\mrightarrow{}  X  with  prod-metric(2;\mlambda{}i.d))
\mvdash{}  \mexists{}delta:\{d:\mBbbR{}|  r0  <  d\}  .  \mforall{}x,y:X.    ((mdist(d;x;y)  \mleq{}  delta)  {}\mRightarrow{}  (mdist(dY;f  x;f  y)  \mleq{}  (r1/r(k))))


By

---

Latex:
((RenameVar  `cmp2'  (-1)  THEN  RenameVar  `mtb2'  (-2))
  THEN  (InstLemma  `compact-metric-to-real-continuity`  [\mkleeneopen{}i:\mBbbN{}2  {}\mrightarrow{}  X\mkleeneclose{};\mkleeneopen{}prod-metric(2;\mlambda{}i.d)\mkleeneclose{};\mkleeneopen{}<cmp2
                                                                                                                                                                                  ,  mtb2
                                                                                                                                                                                  >\mkleeneclose{};
              \mkleeneopen{}\mlambda{}p.mdist(dY;f  (p  0);f  (p  1))\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  MemTypeCD  THEN  Auto  THEN  RepUR  ``is-mfun  so\_apply``  0  THEN  Auto)
              )
  )

---

Home Index