---

Step * 1 1 1 1 1 of Lemma m-closed-iff-complete

.....wf..... 
1. X : Type
2. d : metric(X)
3. ∀x:ℕ ⟶ X. (mcauchy(d;n.x n) ⇒ x n↓ as n→∞)
4. A : Type
5. metric-subspace(X;d;A)
6. d ∈ metric(A)
7. x : ℕ ⟶ A
8. mcauchy(d;n.x n)
9. y : X
10. k : ℕ+
11. N : ℕ
12. ∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k))))
⊢ x N ∈ A
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  X  :  Type
2.  d  :  metric(X)
3.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
4.  A  :  Type
5.  metric-subspace(X;d;A)
6.  d  \mmember{}  metric(A)
7.  x  :  \mBbbN{}  {}\mrightarrow{}  A
8.  mcauchy(d;n.x  n)
9.  y  :  X
10.  k  :  \mBbbN{}\msupplus{}
11.  N  :  \mBbbN{}
12.  \mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (mdist(d;x  n;y)  \mleq{}  (r1/r(k))))
\mvdash{}  x  N  \mmember{}  A


By

---

Latex:
Auto

---

Home Index