---

Step * 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:ℕ. ∃n:ℕ+. ∃xs:ℕn ⟶ X. ∀x:X. ∃i:ℕn. (mdist(dX;x;xs i) ≤ (r1/r(k + 1)))
7. k : ℕ
8. delta : {d:ℝ| r0 < d} 
9. ∀x,y:X.  ((mdist(dX;x;y) ≤ delta) ⇒ (mdist(dY;f x;f y) ≤ (r1/r(k + 1))))
⊢ ∃n:ℕ+. ∃xs:ℕn ⟶ f[X]. ∀x:f[X]. ∃i:ℕn. (mdist(image-metric(dY);x;xs i) ≤ (r1/r(k + 1)))
BY
{ ((InstLemma `small-reciprocal-real` [⌜delta⌝]⋅ THENA Auto)
   THEN D -1
   THEN (D 6 With ⌜k1 - 1⌝  THENA Auto)
   THEN (Subst' (k1 - 1) + 1 ~ k1 -1 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:ℕ+. ∃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)))

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  dX  :  metric(X)
3.  [Y]  :  Type
4.  dY  :  metric(Y)
5.  f  :  X  {}\mrightarrow{}  Y
6.  \mforall{}k:\mBbbN{}.  \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(k  +  1)))
7.  k  :  \mBbbN{}
8.  delta  :  \{d:\mBbbR{}|  r0  <  d\} 
9.  \mforall{}x,y:X.    ((mdist(dX;x;y)  \mleq{}  delta)  {}\mRightarrow{}  (mdist(dY;f  x;f  y)  \mleq{}  (r1/r(k  +  1))))
\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:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}delta\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  6  With  \mkleeneopen{}k1  -  1\mkleeneclose{}    THENA  Auto)
  THEN  (Subst'  (k1  -  1)  +  1  \msim{}  k1  -1  THENA  Auto))

---

Home Index