---

Step * of Lemma rat-cube-complex-polyhedron-compact1

∀k:ℕ. ∀K:ℚCube(k) List.  (0 < ||K|| ⇒ (∀c∈K.↑Inhabited(c)) ⇒ mcompact(|K|;rn-prod-metric(k)))
BY
{ (Intros
   THEN (InstLemma `mcompact-stable-union` [⌜ℝ^k⌝;⌜rn-prod-metric(k)⌝;⌜ℕ||K||⌝;⌜λ2i p.in-rat-cube(k;p;K[i])⌝]⋅
         THENA (Auto THEN Try ((RWO "-1" 0 THEN Auto)))
         )
   ) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. 0 < ||K||
4. (∀c∈K.↑Inhabited(c))
5. i : ℕ||K||
⊢ mcompact({x:ℝ^k| in-rat-cube(k;x;K[i])} ;rn-prod-metric(k))

2
.....antecedent..... 
1. k : ℕ
2. K : ℚCube(k) List
3. 0 < ||K||
4. (∀c∈K.↑Inhabited(c))
⊢ ℕ||K||

3
1. k : ℕ
2. K : ℚCube(k) List
3. 0 < ||K||
4. (∀c∈K.↑Inhabited(c))
5. mcompact(stable-union(ℝ^k;ℕ||K||;i,x.in-rat-cube(k;x;K[i]));rn-prod-metric(k))
⊢ mcompact(|K|;rn-prod-metric(k))

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}K:\mBbbQ{}Cube(k)  List.    (0  <  ||K||  {}\mRightarrow{}  (\mforall{}c\mmember{}K.\muparrow{}Inhabited(c))  {}\mRightarrow{}  mcompact(|K|;rn-prod-metric(k)))


By

---

Latex:
(Intros
  THEN  (InstLemma  `mcompact-stable-union`  [\mkleeneopen{}\mBbbR{}\^{}k\mkleeneclose{};\mkleeneopen{}rn-prod-metric(k)\mkleeneclose{};\mkleeneopen{}\mBbbN{}||K||\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}i  p.in-rat-cube(k;p;K[i])\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))
              )
  )

---

Home Index