---

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

∀k:ℕ. ∀[n:ℕ]. ∀K:n-dim-complex. (0 < ||K|| ⇒ |K|)
BY
{ (Auto THEN RepeatFor 2 (DVar `K') THEN All Reduce THEN Auto) }

1
1. k : ℕ
2. [n] : ℕ
3. u : ℚCube(k)
4. v : ℚCube(k) List
5. [%2] : no_repeats(ℚCube(k);[u / v]) ∧ (∀c,d∈[u / v].  Compatible(c;d)) ∧ (∀c∈[u / v].dim(c) = n ∈ ℤ)
6. 0 < ||v|| + 1
⊢ |[u / v]|

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}[n:\mBbbN{}].  \mforall{}K:n-dim-complex.  (0  <  ||K||  {}\mRightarrow{}  |K|)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (DVar  `K')  THEN  All  Reduce  THEN  Auto)

---

Home Index