---

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


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
⊢ permutation(ℚCube(k);∂((K)');(∂(K))')
BY
{ ((BLemma `equal-rat-cube-complexes` THENW Auto)
   THEN Intro
   THEN (Assert (↑Inhabited(c)) ∧ (dim(c) = (n - 1) ∈ ℤ) BY
               Auto)
   THEN D -2
   THEN Thin (-2)
   THEN RWW "member-rat-complex-boundary-n member-rat-complex-subdiv2" 0⋅
   THEN Auto
   THEN ExRepD) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. c : ℚCube(k)
6. ↑Inhabited(c)
7. dim(c) = (n - 1) ∈ ℤ
8. ↑in-complex-boundary(k;c;(K)')
9. dim(c) = (n - 1) ∈ ℤ
⊢ ∃a:ℚCube(k). (((↑in-complex-boundary(k;a;K)) ∧ (dim(a) = (n - 1) ∈ ℤ)) ∧ (↑is-half-cube(k;c;a)))

2
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. ¬(n = 0 ∈ ℤ)
5. c : ℚCube(k)
6. ↑Inhabited(c)
7. dim(c) = (n - 1) ∈ ℤ
8. a : ℚCube(k)
9. ↑in-complex-boundary(k;a;K)
10. dim(a) = (n - 1) ∈ ℤ
11. ↑is-half-cube(k;c;a)
⊢ ↑in-complex-boundary(k;c;(K)')

---

Latex:

---

Latex:

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


By

---

Latex:
((BLemma  `equal-rat-cube-complexes`  THENW  Auto)
  THEN  Intro
  THEN  (Assert  (\muparrow{}Inhabited(c))  \mwedge{}  (dim(c)  =  (n  -  1))  BY
                          Auto)
  THEN  D  -2
  THEN  Thin  (-2)
  THEN  RWW  "member-rat-complex-boundary-n  member-rat-complex-subdiv2"  0\mcdot{}
  THEN  Auto
  THEN  ExRepD)

---

Home Index