---

Step * 1 of Lemma rat-complex-boundary-subdiv


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. n = 0 ∈ ℤ
⊢ permutation(ℚCube(k);∂((K)');(∂(K))')
BY
{ (RWO "rat-complex-boundary-0-dim" 0 THEN Auto THEN (Subst' ([])' ~ [] 0 THENA Computation) THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  n  =  0
\mvdash{}  permutation(\mBbbQ{}Cube(k);\mpartial{}((K)');(\mpartial{}(K))')


By

---

Latex:
(RWO  "rat-complex-boundary-0-dim"  0
  THEN  Auto
  THEN  (Subst'  ([])'  \msim{}  []  0  THENA  Computation)
  THEN  Auto)

---

Home Index