---

Step * of Lemma mcompact-product

∀k:ℕ. ∀X:ℕk ⟶ Type. ∀d:i:ℕk ⟶ metric(X i).  ((∀i:ℕk. mcompact(X i;d i)) ⇒ mcompact(i:ℕk ⟶ (X i);prod-metric(k;d)))
BY
{ (Auto THEN D 0 THEN Try ((BLemma `m-TB-product` THEN Auto))) }

1
1. k : ℕ
2. X : ℕk ⟶ Type
3. d : i:ℕk ⟶ metric(X i)
4. ∀i:ℕk. mcompact(X i;d i)
⊢ mcomplete(i:ℕk ⟶ (X i) with prod-metric(k;d))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}X:\mBbbN{}k  {}\mrightarrow{}  Type.  \mforall{}d:i:\mBbbN{}k  {}\mrightarrow{}  metric(X  i).
    ((\mforall{}i:\mBbbN{}k.  mcompact(X  i;d  i))  {}\mRightarrow{}  mcompact(i:\mBbbN{}k  {}\mrightarrow{}  (X  i);prod-metric(k;d)))


By

---

Latex:
(Auto  THEN  D  0  THEN  Try  ((BLemma  `m-TB-product`  THEN  Auto)))

---

Home Index