---

Step * of Lemma reals-complete

mcomplete(ℝ with rmetric())
BY
{ (InstLemma `converges-iff-cauchy` []
   THEN RepUR ``mcomplete mcauchy mconverges mconverges-to mdist rmetric`` 0
   THEN Folds ``cauchy converges-to`` 0
   THEN Fold `converges` 0
   THEN Auto) }

---

Latex:

---

Latex:
mcomplete(\mBbbR{}  with  rmetric())


By

---

Latex:
(InstLemma  `converges-iff-cauchy`  []
  THEN  RepUR  ``mcomplete  mcauchy  mconverges  mconverges-to  mdist  rmetric``  0
  THEN  Folds  ``cauchy  converges-to``  0
  THEN  Fold  `converges`  0
  THEN  Auto)

---

Home Index