---

Step * of Lemma prod-metric-space-complete

No Annotations
∀k:ℕ. ∀X:ℕk ⟶ MetricSpace.  ((∀i:ℕk. mcomplete(X i)) ⇒ mcomplete(prod-metric-space(k;X)))
BY
{ (Auto
   THEN (InstLemma `prod-metric_wf` [⌜k⌝;⌜λ2i.fst((X i))⌝;⌜λi.(snd((X i)))⌝]⋅ THENA Auto)
   THEN RepUR ``prod-metric-space mcomplete`` 0
   THEN Auto) }

1
1. k : ℕ
2. X : ℕk ⟶ MetricSpace
3. ∀i:ℕk. mcomplete(X i)
4. prod-metric(k;λi.(snd((X i)))) ∈ metric(i:ℕk ⟶ (fst((X i))))
5. x : ℕ ⟶ i:ℕk ⟶ (fst((X i)))
6. mcauchy(prod-metric(k;λi.(snd((X i))));n.x n)
⊢ x n↓ as n→∞

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}X:\mBbbN{}k  {}\mrightarrow{}  MetricSpace.    ((\mforall{}i:\mBbbN{}k.  mcomplete(X  i))  {}\mRightarrow{}  mcomplete(prod-metric-space(k;X)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `prod-metric\_wf`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.fst((X  i))\mkleeneclose{};\mkleeneopen{}\mlambda{}i.(snd((X  i)))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``prod-metric-space  mcomplete``  0
  THEN  Auto)

---

Home Index