---

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


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. m-closed-subspace(X;d;A)
8. x : ℕ ⟶ A
9. mcauchy(d;n.x n)
10. y : X
11. lim n→∞.x n = y
⊢ ∃y:A. lim n→∞.x n = y
BY
{ ((D 7 With ⌜y⌝  THENA Auto) THEN (D -1 THENM (D 0 With ⌜y⌝  THEN Auto))) }

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

---

Latex:

---

Latex:

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.  m-closed-subspace(X;d;A)
8.  x  :  \mBbbN{}  {}\mrightarrow{}  A
9.  mcauchy(d;n.x  n)
10.  y  :  X
11.  lim  n\mrightarrow{}\minfty{}.x  n  =  y
\mvdash{}  \mexists{}y:A.  lim  n\mrightarrow{}\minfty{}.x  n  =  y


By

---

Latex:
((D  7  With  \mkleeneopen{}y\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  THENM  (D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto)))

---

Home Index