---

Step * of Lemma converges-to-cauchy-mlimit

∀[X:Type]
  ∀d:metric(X). ∀cmplt:mcomplete(X with d). ∀x:ℕ ⟶ X. ∀c:mcauchy(d;n.x n).  lim n→∞.x n = cauchy-mlimit(cmplt;x;c)
BY
{ (Auto
   THEN RepUR ``mcomplete`` 3
   THEN RepUR ``cauchy-mlimit`` 0
   THEN (GenConclTerm ⌜cmplt x c⌝⋅ THENA Auto)
   THEN D -2
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}cmplt:mcomplete(X  with  d).  \mforall{}x:\mBbbN{}  {}\mrightarrow{}  X.  \mforall{}c:mcauchy(d;n.x  n).
        lim  n\mrightarrow{}\minfty{}.x  n  =  cauchy-mlimit(cmplt;x;c)


By

---

Latex:
(Auto
  THEN  RepUR  ``mcomplete``  3
  THEN  RepUR  ``cauchy-mlimit``  0
  THEN  (GenConclTerm  \mkleeneopen{}cmplt  x  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  All  Reduce
  THEN  Auto)

---

Home Index