---

Step * 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:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(dX;x;xs i) ≤ (r1/r(k1)))
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ f[X]. ∀x:f[X]. ∃i:ℕn. (mdist(image-metric(dY);x;xs i) ≤ (r1/r(k + 1)))
BY
{ (ParallelLast
   THEN ExRepD
   THEN (D 0 With ⌜λi.f[xs i]⌝  THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Assert x ∈ f[X] BY
               Declaration)
   THEN D -2
   THEN RenameVar `x' (-2)
   THEN (D -4 With ⌜x⌝  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: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)))

---

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.  \mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  X.  \mforall{}x:X.  \mexists{}i:\mBbbN{}n.  (mdist(dX;x;xs  i)  \mleq{}  (r1/r(k1)))
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}xs:\mBbbN{}n  {}\mrightarrow{}  f[X].  \mforall{}x:f[X].  \mexists{}i:\mBbbN{}n.  (mdist(image-metric(dY);x;xs  i)  \mleq{}  (r1/r(k  +  1)))


By

---

Latex:
(ParallelLast
  THEN  ExRepD
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}i.f[xs  i]\mkleeneclose{}    THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  x  \mmember{}  f[X]  BY
                          Declaration)
  THEN  D  -2
  THEN  RenameVar  `x'  (-2)
  THEN  (D  -4  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto))

---

Home Index