---

Step * 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||)
⊢ ↑isEven(||v2||)
BY
{ ((Assert ↑Inhabited(u) BY
          (Unfold `rat-cube-dimension` -3 THEN SplitOnHypITE -3  THEN Auto))
   THEN (InstLemma `member-rat-cube-faces` [⌜k⌝;⌜u⌝]⋅ THENA 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) ∈ ℤ))
⊢ ↑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||)
\mvdash{}  \muparrow{}isEven(||v2||)


By

---

Latex:
((Assert  \muparrow{}Inhabited(u)  BY
                (Unfold  `rat-cube-dimension`  -3  THEN  SplitOnHypITE  -3    THEN  Auto))
  THEN  (InstLemma  `member-rat-cube-faces`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index