---

Step * of Lemma rat-complex-subdiv-polyhedron

∀[k,n:ℕ]. ∀[K:n-dim-complex].  |(K)'| ≡ |K|
BY
{ (Auto
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (SupposeMore (-1) THENA Auto)
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN ExRepD) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. x : ℝ^k
5. c : ℚCube(k)
6. (c ∈ (K)')
7. in-rat-cube(k;x;c)
⊢ ¬¬(∃c∈K. in-rat-cube(k;x;c))

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. x : ℝ^k
5. c : ℚCube(k)
6. (c ∈ K)
7. in-rat-cube(k;x;c)
⊢ ¬¬(∃c∈(K)'. in-rat-cube(k;x;c))

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:n-dim-complex].    |(K)'|  \mequiv{}  |K|


By

---

Latex:
(Auto
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  ExRepD)

---

Home Index