---

Step * of Lemma mcompact-rat-cube

∀k:ℕ. ∀c:ℚCube(k).  ((↑Inhabited(c)) ⇒ mcompact({x:ℝ^k| in-rat-cube(k;x;c)} ;rn-prod-metric(k)))
BY
{ (Auto
   THEN (InstLemma `mcompact-product` [⌜k⌝;⌜λi.{x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} ⌝;⌜λi.rmetric()⌝]\000C⋅
         THENA Auto
         )
   THEN All Reduce) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. i : ℕk
⊢ mcompact({x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} ;rmetric())

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

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).    ((\muparrow{}Inhabited(c))  {}\mRightarrow{}  mcompact(\{x:\mBbbR{}\^{}k|  in-rat-cube(k;x;c)\}  ;rn-prod-metric(k)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `mcompact-product`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}i.\{x:\mBbbR{}| 
                                                                                            x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\}  \mkleeneclose{};
              \mkleeneopen{}\mlambda{}i.rmetric()\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  All  Reduce)

---

Home Index