---

Step * 2 of Lemma mcompact-rat-cube


1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. mcompact(i:ℕk ⟶ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} ;prod-metric(k;λi.rmetric()))
⊢ mcompact({x:ℝ^k| in-rat-cube(k;x;c)} ;rn-prod-metric(k))
BY
{ Fold `rn-prod-metric` (-1) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. mcompact(i:ℕk ⟶ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} ;rn-prod-metric(k))
⊢ mcompact({x:ℝ^k| in-rat-cube(k;x;c)} ;rn-prod-metric(k))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \muparrow{}Inhabited(c)
4.  mcompact(i:\mBbbN{}k  {}\mrightarrow{}  \{x:\mBbbR{}| 
                                          x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\}  ;prod-metric(k;\mlambda{}i.rmetric()))
\mvdash{}  mcompact(\{x:\mBbbR{}\^{}k|  in-rat-cube(k;x;c)\}  ;rn-prod-metric(k))


By

---

Latex:
Fold  `rn-prod-metric`  (-1)

---

Home Index