---

Step * of Lemma rn-metric-complete

∀n:ℕ. mcomplete(ℝ^n with rn-metric(n))
BY
{ ((Auto THEN InstLemma `equiv-metrics-preserve-complete` [⌜ℝ^n⌝;⌜prod-metric(n;λi.rmetric())⌝;⌜rn-metric(n)⌝]⋅)
   THEN Auto
   THEN Try ((Fold `rn-prod-metric` 0 THEN Auto))
   THEN CaseNat 0 `n') }

1
1. n : ℕ
2. n = 0 ∈ ℤ
⊢ ∃c1,c2:{s:ℝ| r0 < s} . (c1*rn-prod-metric(0) ≤ rn-metric(0) ∧ c2*rn-metric(0) ≤ rn-prod-metric(0))

2
1. n : ℕ
2. ¬(n = 0 ∈ ℤ)
⊢ ∃c1,c2:{s:ℝ| r0 < s} . (c1*rn-prod-metric(n) ≤ rn-metric(n) ∧ c2*rn-metric(n) ≤ rn-prod-metric(n))

---

Latex:

---

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


By

---

Latex:
((Auto
    THEN  InstLemma  `equiv-metrics-preserve-complete`  [\mkleeneopen{}\mBbbR{}\^{}n\mkleeneclose{};\mkleeneopen{}prod-metric(n;\mlambda{}i.rmetric())\mkleeneclose{};
              \mkleeneopen{}rn-metric(n)\mkleeneclose{}]\mcdot{}
    )
  THEN  Auto
  THEN  Try  ((Fold  `rn-prod-metric`  0  THEN  Auto))
  THEN  CaseNat  0  `n')

---

Home Index