---

Step * of Lemma cauchy-mlimit-unique

∀[X:Type]. ∀[d:metric(X)]. ∀[cmplt:mcomplete(X with d)]. ∀[x:ℕ ⟶ X]. ∀[c:mcauchy(d;n.x n)]. ∀[z:X].
  cauchy-mlimit(cmplt;x;c) ≡ z supposing lim n→∞.x n = z
BY
{ (InstLemma `converges-to-cauchy-mlimit` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN FLemma `m-unique-limit` [-3; -1]
   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)].  \mforall{}[z:X].
    cauchy-mlimit(cmplt;x;c)  \mequiv{}  z  supposing  lim  n\mrightarrow{}\minfty{}.x  n  =  z


By

---

Latex:
(InstLemma  `converges-to-cauchy-mlimit`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  FLemma  `m-unique-limit`  [-3;  -1]
  THEN  Auto)

---

Home Index