---

Step * 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)
⊢ mcomplete(i:ℕk ⟶ (X i) with prod-metric(k;d))
BY
{ (InstLemma `prod-metric-space-complete` [⌜k⌝;⌜λi.X i with d i⌝]⋅
   THENA (Auto THEN Reduce 0 THEN (D -2 With ⌜i⌝  THENA Auto) THEN D -1 THEN Auto)
   ) }

1
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))

---

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)
\mvdash{}  mcomplete(i:\mBbbN{}k  {}\mrightarrow{}  (X  i)  with  prod-metric(k;d))


By

---

Latex:
(InstLemma  `prod-metric-space-complete`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}i.X  i  with  d  i\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  Reduce  0  THEN  (D  -2  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  D  -1  THEN  Auto)
  )

---

Home Index