---

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


1. k : ℕ
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. j : ℤ
5. [%3] : 0 < j
6. K : n-dim-complex
7. v : n - 1-dim-complex
8. ∂(K'^(j - 1)) = v ∈ n - 1-dim-complex
9. v1 : n - 1-dim-complex
10. ∂(K)'^(j - 1) = v1 ∈ n - 1-dim-complex
11. v2 : n - 1-dim-complex
12. ∂((K'^(j - 1))') = v2 ∈ n - 1-dim-complex
13. permutation(ℚCube(k);v2;(v)')
14. permutation(ℚCube(k);v;v1)
⊢ permutation(ℚCube(k);v2;(v1)')
BY
{ (InstLemma `permutation_transitivity` [⌜ℚCube(k)⌝;⌜v2⌝;⌜(v)'⌝;⌜(v1)'⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. k : ℕ
2. n : ℕ
3. ¬(n = 0 ∈ ℤ)
4. j : ℤ
5. [%3] : 0 < j
6. K : n-dim-complex
7. v : n - 1-dim-complex
8. ∂(K'^(j - 1)) = v ∈ n - 1-dim-complex
9. v1 : n - 1-dim-complex
10. ∂(K)'^(j - 1) = v1 ∈ n - 1-dim-complex
11. v2 : n - 1-dim-complex
12. ∂((K'^(j - 1))') = v2 ∈ n - 1-dim-complex
13. permutation(ℚCube(k);v2;(v)')
14. permutation(ℚCube(k);v;v1)
⊢ permutation(ℚCube(k);(v)';(v1)')

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  \mneg{}(n  =  0)
4.  j  :  \mBbbZ{}
5.  [\%3]  :  0  <  j
6.  K  :  n-dim-complex
7.  v  :  n  -  1-dim-complex
8.  \mpartial{}(K'\^{}(j  -  1))  =  v
9.  v1  :  n  -  1-dim-complex
10.  \mpartial{}(K)'\^{}(j  -  1)  =  v1
11.  v2  :  n  -  1-dim-complex
12.  \mpartial{}((K'\^{}(j  -  1))')  =  v2
13.  permutation(\mBbbQ{}Cube(k);v2;(v)')
14.  permutation(\mBbbQ{}Cube(k);v;v1)
\mvdash{}  permutation(\mBbbQ{}Cube(k);v2;(v1)')


By

---

Latex:
(InstLemma  `permutation\_transitivity`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{};\mkleeneopen{}(v)'\mkleeneclose{};\mkleeneopen{}(v1)'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index