---

Step * 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))))
⊢ ↑isEven(||v2||)
BY
{ ((Assert ↑isEven(||rat-cube-faces(k;u)||) BY
          (RWO "length-rat-cube-faces" 0 THEN Auto THEN RWO "isEven-2n" 0 THEN Auto))
   THEN (InstLemma `no_repeats-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) ∈ ℤ))
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||)

---

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


By

---

Latex:
((Assert  \muparrow{}isEven(||rat-cube-faces(k;u)||)  BY
                (RWO  "length-rat-cube-faces"  0  THEN  Auto  THEN  RWO  "isEven-2n"  0  THEN  Auto))
  THEN  (InstLemma  `no\_repeats-rat-cube-faces`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index