---

Step * 1 of Lemma mcompact_functionality


1. [X] : Type
2. [Y] : Type
3. X ≡ Y
4. d : metric(X)
5. m-TB(X;d)
6. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
⊢ ∀x:ℕ ⟶ Y. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
BY
{ RepeatFor 4 (ParallelLast) }

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [Y]  :  Type
3.  X  \mequiv{}  Y
4.  d  :  metric(X)
5.  m-TB(X;d)
6.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
\mvdash{}  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  Y.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})


By

---

Latex:
RepeatFor  4  (ParallelLast)

---

Home Index