---

Step * 1 1 of Lemma mcompact-product


1. k : ℕ
2. X : ℕk ⟶ Type
3. d : i:ℕk ⟶ metric(X i)
4. ∀i:ℕk. mcompact(X i;d i)
5. mcomplete(prod-metric-space(k;λi.X i with d i))
⊢ mcomplete(i:ℕk ⟶ (X i) with prod-metric(k;d))
BY
{ (RepUR ``prod-metric-space mk-metric-space`` -1 THEN Subst' (λi.(d i)) = d ∈ (i:ℕk ⟶ metric(X i)) -1 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  X  :  \mBbbN{}k  {}\mrightarrow{}  Type
3.  d  :  i:\mBbbN{}k  {}\mrightarrow{}  metric(X  i)
4.  \mforall{}i:\mBbbN{}k.  mcompact(X  i;d  i)
5.  mcomplete(prod-metric-space(k;\mlambda{}i.X  i  with  d  i))
\mvdash{}  mcomplete(i:\mBbbN{}k  {}\mrightarrow{}  (X  i)  with  prod-metric(k;d))


By

---

Latex:
(RepUR  ``prod-metric-space  mk-metric-space``  -1  THEN  Subst'  (\mlambda{}i.(d  i))  =  d  -1  THEN  Auto)

---

Home Index