---

Step * 1 1 1 of Lemma continuous-image-m-TB


1. [X] : Type
2. dX : metric(X)
3. [Y] : Type
4. dY : metric(Y)
5. f : X ⟶ Y
6. k : ℕ
7. delta : {d:ℝ| r0 < d} 
8. ∀x,y:X.  ((mdist(dX;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k + 1))))
9. k1 : ℕ+
10. (r1/r(k1)) < delta
11. n : ℕ+
12. xs : ℕn ⟶ X
13. y : Y
14. x : {x:X| y ≡ f x} 
15. <y, x> ∈ f[X]
16. ∃i:ℕn. (mdist(dX;x;xs i) ≤ (r1/r(k1)))
⊢ ∃i:ℕn. (mdist(image-metric(dY);<y, x>;(λi.f[xs i]) i) ≤ (r1/r(k + 1)))
BY
{ ((ParallelLast THEN Reduce 0)
   THEN (InstHyp [⌜x⌝;⌜xs i⌝] 8⋅ THENA Auto)
   THEN RepUR ``mdist image-metric image-ap`` 0
   THEN Fold `mdist` 0) }

1
1. [X] : Type
2. dX : metric(X)
3. [Y] : Type
4. dY : metric(Y)
5. f : X ⟶ Y
6. k : ℕ
7. delta : {d:ℝ| r0 < d} 
8. ∀x,y:X.  ((mdist(dX;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k + 1))))
9. k1 : ℕ+
10. (r1/r(k1)) < delta
11. n : ℕ+
12. xs : ℕn ⟶ X
13. y : Y
14. x : {x:X| y ≡ f x} 
15. <y, x> ∈ f[X]
16. i : ℕn
17. mdist(dX;x;xs i) ≤ (r1/r(k1))
18. mdist(dY;f x;f (xs i)) ≤ (r1/r(k + 1))
⊢ mdist(dY;y;f (xs i)) ≤ (r1/r(k + 1))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  dX  :  metric(X)
3.  [Y]  :  Type
4.  dY  :  metric(Y)
5.  f  :  X  {}\mrightarrow{}  Y
6.  k  :  \mBbbN{}
7.  delta  :  \{d:\mBbbR{}|  r0  <  d\} 
8.  \mforall{}x,y:X.    ((mdist(dX;x;y)  \mleq{}  delta)  {}\mRightarrow{}  (mdist(dY;f  x;f  y)  \mleq{}  (r1/r(k  +  1))))
9.  k1  :  \mBbbN{}\msupplus{}
10.  (r1/r(k1))  <  delta
11.  n  :  \mBbbN{}\msupplus{}
12.  xs  :  \mBbbN{}n  {}\mrightarrow{}  X
13.  y  :  Y
14.  x  :  \{x:X|  y  \mequiv{}  f  x\} 
15.  <y,  x>  \mmember{}  f[X]
16.  \mexists{}i:\mBbbN{}n.  (mdist(dX;x;xs  i)  \mleq{}  (r1/r(k1)))
\mvdash{}  \mexists{}i:\mBbbN{}n.  (mdist(image-metric(dY);<y,  x>(\mlambda{}i.f[xs  i])  i)  \mleq{}  (r1/r(k  +  1)))


By

---

Latex:
((ParallelLast  THEN  Reduce  0)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}xs  i\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
  THEN  RepUR  ``mdist  image-metric  image-ap``  0
  THEN  Fold  `mdist`  0)

---

Home Index