---

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

∀k:ℕ. ∀[n:ℕ]. ∀K:{K:n-dim-complex| 0 < ||K||} . mcompact(|K|;rn-prod-metric(k))
BY
{ (Auto
   THEN (Assert (∀c∈K.↑Inhabited(c)) BY
               (RepeatFor 2 (DVar `K')
                THEN Unhide
                THEN Auto
                THEN RepeatFor 2 (ParallelOp -2)
                THEN Unfold `rat-cube-dimension` -1
                THEN SplitOnHypITE -1 
                THEN Auto))
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}[n:\mBbbN{}].  \mforall{}K:\{K:n-dim-complex|  0  <  ||K||\}  .  mcompact(|K|;rn-prod-metric(k))


By

---

Latex:
(Auto
  THEN  (Assert  (\mforall{}c\mmember{}K.\muparrow{}Inhabited(c))  BY
                          (RepeatFor  2  (DVar  `K')
                            THEN  Unhide
                            THEN  Auto
                            THEN  RepeatFor  2  (ParallelOp  -2)
                            THEN  Unfold  `rat-cube-dimension`  -1
                            THEN  SplitOnHypITE  -1 
                            THEN  Auto))
  THEN  EAuto  1)

---

Home Index