---

Step * 1 1 1 1 1 of Lemma length-rat-complex-boundary-even


1. k : ℕ
2. u : ℚCube(k)
3. j : ℕ
4. v1 : j-dim-complex
5. v2 : j-dim-complex
6. dim(u) = (j + 1) ∈ ℤ
7. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬f ≤ u)) ∨ ((¬(f ∈ v2)) ∧ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ)))
8. ↑isEven(||v1||)
9. ↑Inhabited(u)
10. ∀f:ℚCube(k). ((f ∈ rat-cube-faces(k;u)) ⇐⇒ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ))
11. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ rat-cube-faces(k;u)))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ rat-cube-faces(k;u))))
12. ↑isEven(||rat-cube-faces(k;u)||)
13. no_repeats(ℚCube(k);rat-cube-faces(k;u))
⊢ ↑isEven(||v2||)
BY
{ (DVar `v1' THEN DVar `v2' THEN (Unhide THENA Auto) THEN ExRepD) }

1
1. k : ℕ
2. u : ℚCube(k)
3. j : ℕ
4. v1 : ℚCube(k) List
5. no_repeats(ℚCube(k);v1)
6. (∀c,d∈v1.  Compatible(c;d))
7. (∀c∈v1.dim(c) = j ∈ ℤ)
8. v2 : ℚCube(k) List
9. no_repeats(ℚCube(k);v2)
10. (∀c,d∈v2.  Compatible(c;d))
11. (∀c∈v2.dim(c) = j ∈ ℤ)
12. dim(u) = (j + 1) ∈ ℤ
13. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬f ≤ u)) ∨ ((¬(f ∈ v2)) ∧ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ)))
14. ↑isEven(||v1||)
15. ↑Inhabited(u)
16. ∀f:ℚCube(k). ((f ∈ rat-cube-faces(k;u)) ⇐⇒ f ≤ u ∧ (dim(f) = (dim(u) - 1) ∈ ℤ))
17. ∀f:ℚCube(k). ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ rat-cube-faces(k;u)))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ rat-cube-faces(k;u))))
18. ↑isEven(||rat-cube-faces(k;u)||)
19. no_repeats(ℚCube(k);rat-cube-faces(k;u))
⊢ ↑isEven(||v2||)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  u  :  \mBbbQ{}Cube(k)
3.  j  :  \mBbbN{}
4.  v1  :  j-dim-complex
5.  v2  :  j-dim-complex
6.  dim(u)  =  (j  +  1)
7.  \mforall{}f:\mBbbQ{}Cube(k)
          ((f  \mmember{}  v1)  \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  v2)  \mwedge{}  (\mneg{}f  \mleq{}  u))  \mvee{}  ((\mneg{}(f  \mmember{}  v2))  \mwedge{}  f  \mleq{}  u  \mwedge{}  (dim(f)  =  (dim(u)  -  1))))
8.  \muparrow{}isEven(||v1||)
9.  \muparrow{}Inhabited(u)
10.  \mforall{}f:\mBbbQ{}Cube(k).  ((f  \mmember{}  rat-cube-faces(k;u))  \mLeftarrow{}{}\mRightarrow{}  f  \mleq{}  u  \mwedge{}  (dim(f)  =  (dim(u)  -  1)))
11.  \mforall{}f:\mBbbQ{}Cube(k)
            ((f  \mmember{}  v1)
            \mLeftarrow{}{}\mRightarrow{}  ((f  \mmember{}  v2)  \mwedge{}  (\mneg{}(f  \mmember{}  rat-cube-faces(k;u))))  \mvee{}  ((\mneg{}(f  \mmember{}  v2))  \mwedge{}  (f  \mmember{}  rat-cube-faces(k;u))))
12.  \muparrow{}isEven(||rat-cube-faces(k;u)||)
13.  no\_repeats(\mBbbQ{}Cube(k);rat-cube-faces(k;u))
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
(DVar  `v1'  THEN  DVar  `v2'  THEN  (Unhide  THENA  Auto)  THEN  ExRepD)

---

Home Index