---

Step * 1 of Lemma metric-leq-complete


1. [X] : Type
2. [d1] : metric(X)
3. [d2] : metric(X)
4. d2 ≤ d1
5. ∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x[n] = y ⇒ lim n→∞.x[n] = y)
6. ∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ (∃y:ℕ ⟶ X. (subsequence(a,b.a ≡ b;n.x n;n.y n) ∧ mcauchy(d1;n.y n))))
7. ∀x:ℕ ⟶ X. (mcauchy(d1;n.x n) ⇒ x n↓ as n→∞)
8. x : ℕ ⟶ X
9. mcauchy(d2;n.x n)
⊢ x n↓ as n→∞
BY
{ ((InstHyp [⌜x⌝] (-4)⋅ THEN Auto)
   THEN ExRepD
   THEN InstHyp [⌜y⌝] (-6)⋅
   THEN Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN RenameVar `a' (-2)) }

1
1. [X] : Type
2. [d1] : metric(X)
3. [d2] : metric(X)
4. d2 ≤ d1
5. ∀x:ℕ ⟶ X. ∀y:X.  (lim n→∞.x[n] = y ⇒ lim n→∞.x[n] = y)
6. ∀x:ℕ ⟶ X. (mcauchy(d2;n.x n) ⇒ (∃y:ℕ ⟶ X. (subsequence(a,b.a ≡ b;n.x n;n.y n) ∧ mcauchy(d1;n.y n))))
7. ∀x:ℕ ⟶ X. (mcauchy(d1;n.x n) ⇒ x n↓ as n→∞)
8. x : ℕ ⟶ X
9. mcauchy(d2;n.x n)
10. y : ℕ ⟶ X
11. subsequence(a,b.a ≡ b;n.x n;n.y n)
12. mcauchy(d1;n.y n)
13. a : X
14. lim n→∞.y n = a
⊢ lim n→∞.x n = a

---

Latex:

---

Latex:

1.  [X]  :  Type
2.  [d1]  :  metric(X)
3.  [d2]  :  metric(X)
4.  d2  \mleq{}  d1
5.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  \mforall{}y:X.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  y  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  =  y)
6.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X
          (mcauchy(d2;n.x  n)  {}\mRightarrow{}  (\mexists{}y:\mBbbN{}  {}\mrightarrow{}  X.  (subsequence(a,b.a  \mequiv{}  b;n.x  n;n.y  n)  \mwedge{}  mcauchy(d1;n.y  n))))
7.  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  (mcauchy(d1;n.x  n)  {}\mRightarrow{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{})
8.  x  :  \mBbbN{}  {}\mrightarrow{}  X
9.  mcauchy(d2;n.x  n)
\mvdash{}  x  n\mdownarrow{}  as  n\mrightarrow{}\minfty{}


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-6)\mcdot{}
  THEN  Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  RenameVar  `a'  (-2))

---

Home Index