---

Step * 2 1 1 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)
⊢ ∀x:ℚCube(k). ((x ∈ (v1)') ⇐⇒ (x ∈ (v)'))
BY
{ (FLemma `member-permutation` [-1] THENA 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)
15. ∀a:ℚCube(k). ((a ∈ v) ⇐⇒ (a ∈ v1))
⊢ ∀x:ℚCube(k). ((x ∈ (v1)') ⇐⇒ (x ∈ (v)'))

---

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{}  \mforall{}x:\mBbbQ{}Cube(k).  ((x  \mmember{}  (v1)')  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  (v)'))


By

---

Latex:
(FLemma  `member-permutation`  [-1]  THENA  Auto)

---

Home Index