---

Step * 1 1 of Lemma rat-complex-boundary_wf


1. k : ℕ
2. K : ℚCube(k) List
3. no_repeats(ℚCube(k);K) ∧ (∀c,d∈K.  Compatible(c;d)) ∧ (∀c∈K.dim(c) = 0 ∈ ℤ)
⊢ ∂(K) ∈ 0 - 1-dim-complex
BY
{ (RepeatFor 2 (D -1) THEN (RWO "boundary-of-0-dim-is-nil" 0 THENW Auto) THEN (Trivial ORELSE (MemTypeCD THEN Auto))) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  no\_repeats(\mBbbQ{}Cube(k);K)  \mwedge{}  (\mforall{}c,d\mmember{}K.    Compatible(c;d))  \mwedge{}  (\mforall{}c\mmember{}K.dim(c)  =  0)
\mvdash{}  \mpartial{}(K)  \mmember{}  0  -  1-dim-complex


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  (RWO  "boundary-of-0-dim-is-nil"  0  THENW  Auto)
  THEN  (Trivial  ORELSE  (MemTypeCD  THEN  Auto)))

---

Home Index