---

Step * 1 1 2 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. mtb2 : m-TB(i:ℕ2 ⟶ X;prod-metric(2;λ2i.d))
11. cmp2 : mcomplete(i:ℕ2 ⟶ X with prod-metric(2;λi.d))
12. ∀k:ℕ+
      ∃delta:{d:ℝ| r0 < d} 
       ∀x,y:i:ℕ2 ⟶ X.
         ((mdist(prod-metric(2;λi.d);x;y) ≤ delta)
         ⇒ (|mdist(dY;f (x 0);f (x 1)) - mdist(dY;f (y 0);f (y 1))| ≤ (r1/r(k))))
⊢ ∃delta:{d:ℝ| r0 < d} . ∀x,y:X.  ((mdist(d;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k))))
BY
{ ((D -1 With ⌜k⌝  THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN InstHyp [⌜λi.if (i =z 0) then x else y fi ⌝;⌜λi.x⌝] (-4)⋅
   THEN Auto) }

1
.....antecedent..... 
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. delta : {d:ℝ| r0 < d} 
13. ∀x,y:i:ℕ2 ⟶ X.
      ((mdist(prod-metric(2;λi.d);x;y) ≤ delta)
      ⇒ (|mdist(dY;f (x 0);f (x 1)) - mdist(dY;f (y 0);f (y 1))| ≤ (r1/r(k))))
14. x : X
15. y : X
16. mdist(d;x;y) ≤ delta
⊢ mdist(prod-metric(2;λi.d);λi.if (i =z 0) then x else y fi ;λi.x) ≤ delta

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. delta : {d:ℝ| r0 < d} 
13. ∀x,y:i:ℕ2 ⟶ X.
      ((mdist(prod-metric(2;λi.d);x;y) ≤ delta)
      ⇒ (|mdist(dY;f (x 0);f (x 1)) - mdist(dY;f (y 0);f (y 1))| ≤ (r1/r(k))))
14. x : X
15. y : X
16. mdist(d;x;y) ≤ delta
17. |mdist(dY;f ((λi.if (i =z 0) then x else y fi ) 0);f ((λi.if (i =z 0) then x else y fi ) 1)) 
- mdist(dY;f ((λi.x) 0);f ((λi.x) 1))| ≤ (r1/r(k))
⊢ 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.  mtb2  :  m-TB(i:\mBbbN{}2  {}\mrightarrow{}  X;prod-metric(2;\mlambda{}\msubtwo{}i.d))
11.  cmp2  :  mcomplete(i:\mBbbN{}2  {}\mrightarrow{}  X  with  prod-metric(2;\mlambda{}i.d))
12.  \mforall{}k:\mBbbN{}\msupplus{}
            \mexists{}delta:\{d:\mBbbR{}|  r0  <  d\} 
              \mforall{}x,y:i:\mBbbN{}2  {}\mrightarrow{}  X.
                  ((mdist(prod-metric(2;\mlambda{}i.d);x;y)  \mleq{}  delta)
                  {}\mRightarrow{}  (|mdist(dY;f  (x  0);f  (x  1))  -  mdist(dY;f  (y  0);f  (y  1))|  \mleq{}  (r1/r(k))))
\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:
((D  -1  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  x  else  y  fi  \mkleeneclose{};\mkleeneopen{}\mlambda{}i.x\mkleeneclose{}]  (-4)\mcdot{}
  THEN  Auto)

---

Home Index