---

Step * 1 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
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))
BY
{ (DVar `x' THEN (Unhide THENA Auto)) }

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
15. y ≡ f x
16. <y, x> ∈ f[X]
17. i : ℕn
18. mdist(dX;x;xs i) ≤ (r1/r(k1))
19. 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.  i  :  \mBbbN{}n
17.  mdist(dX;x;xs  i)  \mleq{}  (r1/r(k1))
18.  mdist(dY;f  x;f  (xs  i))  \mleq{}  (r1/r(k  +  1))
\mvdash{}  mdist(dY;y;f  (xs  i))  \mleq{}  (r1/r(k  +  1))


By

---

Latex:
(DVar  `x'  THEN  (Unhide  THENA  Auto))

---

Home Index