---

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


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))
BY
{ (Assert ⌜stable-union(ℝ^k;ℕ||K||;i,x.in-rat-cube(k;x;K[i])) ≡ |K|⌝⋅ THENM (RWO "-1" (-2) THEN Auto)) }

1
.....assertion..... 
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))
⊢ stable-union(ℝ^k;ℕ||K||;i,x.in-rat-cube(k;x;K[i])) ≡ |K|

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  0  <  ||K||
4.  (\mforall{}c\mmember{}K.\muparrow{}Inhabited(c))
5.  mcompact(stable-union(\mBbbR{}\^{}k;\mBbbN{}||K||;i,x.in-rat-cube(k;x;K[i]));rn-prod-metric(k))
\mvdash{}  mcompact(|K|;rn-prod-metric(k))


By

---

Latex:
(Assert  \mkleeneopen{}stable-union(\mBbbR{}\^{}k;\mBbbN{}||K||;i,x.in-rat-cube(k;x;K[i]))  \mequiv{}  |K|\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  (-2)  THEN  Auto))

---

Home Index