---

Step * of Lemma metric-leq-complete

No Annotations
∀[X:Type]. ∀[d1,d2:metric(X)].
  (d2 ≤ d1
  ⇒ (∀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)))))
  ⇒ mcomplete(X with d1)
  ⇒ mcomplete(X with d2))
BY
{ (InstLemma `metric-leq-converges-to` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN RepUR ``mcomplete`` 0
   THEN Auto) }

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)
⊢ x n↓ as n→∞

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d1,d2:metric(X)].
    (d2  \mleq{}  d1
    {}\mRightarrow{}  (\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)))))
    {}\mRightarrow{}  mcomplete(X  with  d1)
    {}\mRightarrow{}  mcomplete(X  with  d2))


By

---

Latex:
(InstLemma  `metric-leq-converges-to`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  RepUR  ``mcomplete``  0
  THEN  Auto)

---

Home Index