---

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

.....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)')
BY
{ ((BLemma `permutation-when-no_repeats` THENW Auto)
   THEN Try ((GenConclAtAddr [2] THEN D -2 THEN Unhide THEN Complete (Auto)))
   ) }

1
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)
⊢ ∀x:ℚCube(k). ((x ∈ (v1)') ⇐⇒ (x ∈ (v)'))

---

Latex:

---

Latex:
.....antecedent..... 
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);(v)';(v1)')


By

---

Latex:
((BLemma  `permutation-when-no\_repeats`  THENW  Auto)
  THEN  Try  ((GenConclAtAddr  [2]  THEN  D  -2  THEN  Unhide  THEN  Complete  (Auto)))
  )

---

Home Index