---

Step * 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) ∈ ℤ))
⊢ ↑isEven(||v2||)
BY
{ (Assert ∀f:ℚCube(k)
            ((f ∈ v1) ⇐⇒ ((f ∈ v2) ∧ (¬(f ∈ rat-cube-faces(k;u)))) ∨ ((¬(f ∈ v2)) ∧ (f ∈ rat-cube-faces(k;u)))) BY
         ((RWO "-4 -1" 0 THENA Auto)
          THEN HypSubst' (-5) 0
          THEN (Subst' (j + 1) - 1 ~ j 0 THENA Auto)
          THEN (Assert ∀f:ℚCube(k). ((f ∈ v2) ⇒ (dim(f) = j ∈ ℤ)) BY
                      (Auto THEN DVar `v2' THEN Auto THEN RWO "l_all_iff" 8 THEN Auto))
          THEN Intro
          THEN (RepeatFor 2 (D 0) THENA Auto)
          THEN ParallelLast
          THEN Auto)) }

1
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))))
⊢ ↑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)))
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
(Assert  \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))))  BY
              ((RWO  "-4  -1"  0  THENA  Auto)
                THEN  HypSubst'  (-5)  0
                THEN  (Subst'  (j  +  1)  -  1  \msim{}  j  0  THENA  Auto)
                THEN  (Assert  \mforall{}f:\mBbbQ{}Cube(k).  ((f  \mmember{}  v2)  {}\mRightarrow{}  (dim(f)  =  j))  BY
                                        (Auto  THEN  DVar  `v2'  THEN  Auto  THEN  RWO  "l\_all\_iff"  8  THEN  Auto))
                THEN  Intro
                THEN  (RepeatFor  2  (D  0)  THENA  Auto)
                THEN  ParallelLast
                THEN  Auto))

---

Home Index