---

Step * of Lemma mcomplete-rn-prod-metric

∀n:ℕ. mcomplete(ℝ^n with rn-prod-metric(n))
BY
{ (Auto
   THEN (InstLemma `prod-metric-space-complete` [⌜n⌝;⌜λi.ℝ with rmetric()⌝]⋅ THENA (Reduce 0 THEN Auto))
   THEN ParallelLast
   THEN RepUR ``prod-metric-space mk-metric-space`` -1
   THEN Folds ``real-vec rn-prod-metric`` (-1)
   THEN RepUR ``mk-metric-space`` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  mcomplete(\mBbbR{}\^{}n  with  rn-prod-metric(n))


By

---

Latex:
(Auto
  THEN  (InstLemma  `prod-metric-space-complete`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}i.\mBbbR{}  with  rmetric()\mkleeneclose{}]\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              )
  THEN  ParallelLast
  THEN  RepUR  ``prod-metric-space  mk-metric-space``  -1
  THEN  Folds  ``real-vec  rn-prod-metric``  (-1)
  THEN  RepUR  ``mk-metric-space``  0
  THEN  Trivial)

---

Home Index