---

Step * of Lemma continuous-image-m-TB

∀[X:Type]
  ∀dX:metric(X). ∀[Y:Type]. ∀dY:metric(Y). ∀f:X ⟶ Y.  (UC(f:X ⟶ Y) ⇒ m-TB(X;dX) ⇒ m-TB(f[X];image-metric(dY)))
BY
{ (Auto
   THEN (BLemma `m-TB-iff` THENA Auto)
   THEN (RWO "m-TB-iff" (-1) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (D -3 With ⌜k + 1⌝  THENA Auto)
   THEN D -1) }

1
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)))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}dX:metric(X)
        \mforall{}[Y:Type]
            \mforall{}dY:metric(Y).  \mforall{}f:X  {}\mrightarrow{}  Y.    (UC(f:X  {}\mrightarrow{}  Y)  {}\mRightarrow{}  m-TB(X;dX)  {}\mRightarrow{}  m-TB(f[X];image-metric(dY)))


By

---

Latex:
(Auto
  THEN  (BLemma  `m-TB-iff`  THENA  Auto)
  THEN  (RWO  "m-TB-iff"  (-1)  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -3  With  \mkleeneopen{}k  +  1\mkleeneclose{}    THENA  Auto)
  THEN  D  -1)

---

Home Index