---

Step * of Lemma rat-complex-boundary-subdiv

No Annotations
∀k,n:ℕ. ∀K:n-dim-complex.  permutation(ℚCube(k);∂((K)');(∂(K))')
BY
{ (Auto THEN CaseNat 0 `n') }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. n = 0 ∈ ℤ
⊢ permutation(ℚCube(k);∂((K)');(∂(K))')

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
⊢ permutation(ℚCube(k);∂((K)');(∂(K))')

---

Latex:

---

Latex:
No  Annotations
\mforall{}k,n:\mBbbN{}.  \mforall{}K:n-dim-complex.    permutation(\mBbbQ{}Cube(k);\mpartial{}((K)');(\mpartial{}(K))')


By

---

Latex:
(Auto  THEN  CaseNat  0  `n')

---

Home Index