---

Step * of Lemma boundary-of-0-dim-is-nil

∀[k:ℕ]. ∀[K:ℚCube(k) List].  ∂(K) ~ [] supposing (∀c∈K.dim(c) = 0 ∈ ℤ)
BY
{ (Auto
   THEN RepUR ``rat-complex-boundary rat-cube-sub-complex`` 0
   THEN (Subst' face-complex(k;K) ~ [] 0 THENM (Reduce 0 THEN Auto))) }

1
.....equality..... 
1. k : ℕ
2. K : ℚCube(k) List
3. (∀c∈K.dim(c) = 0 ∈ ℤ)
⊢ face-complex(k;K) ~ []

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[K:\mBbbQ{}Cube(k)  List].    \mpartial{}(K)  \msim{}  []  supposing  (\mforall{}c\mmember{}K.dim(c)  =  0)


By

---

Latex:
(Auto
  THEN  RepUR  ``rat-complex-boundary  rat-cube-sub-complex``  0
  THEN  (Subst'  face-complex(k;K)  \msim{}  []  0  THENM  (Reduce  0  THEN  Auto)))

---

Home Index