---

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

.....antecedent..... 
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. lim n→∞.x n = y
⊢ ∀k:ℕ+. ∃a:A. (mdist(d;y;a) ≤ (r1/r(k)))
BY
{ ((D 0 THENA Auto) THEN (D -2 With ⌜k⌝  THENA Auto) THEN D -1) }

1
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. [%11] : ∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x n;y) ≤ (r1/r(k))))
⊢ ∃a:A. (mdist(d;y;a) ≤ (r1/r(k)))

---

Latex:

---

Latex:
.....antecedent..... 
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.  lim  n\mrightarrow{}\minfty{}.x  n  =  y
\mvdash{}  \mforall{}k:\mBbbN{}\msupplus{}.  \mexists{}a:A.  (mdist(d;y;a)  \mleq{}  (r1/r(k)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (D  -2  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)  THEN  D  -1)

---

Home Index