---

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


1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 2 ≤ n
5. ∀[L:ℚCube(k) List]. L ~ [] supposing ∀x:ℚCube(k). (¬(x ∈ L))
6. x : ℚCube(k)
7. (x ∈ ∂(∂(K)))
⊢ False
BY
{ ((InstLemma `member-rat-complex-boundary-n` [⌜n - 1⌝]⋅ THENA Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-1)
   THEN RepUR ``in-complex-boundary`` -1
   THEN D -1) }

1
1. k : ℕ
2. n : ℕ
3. K : n-dim-complex
4. 2 ≤ n
5. ∀[L:ℚCube(k) List]. L ~ [] supposing ∀x:ℚCube(k). (¬(x ∈ L))
6. x : ℚCube(k)
7. ↑isOdd(||filter(λc.is-rat-cube-face(k;x;c);∂(K))||)
8. dim(x) = (n - 1 - 1) ∈ ℤ
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  n-dim-complex
4.  2  \mleq{}  n
5.  \mforall{}[L:\mBbbQ{}Cube(k)  List].  L  \msim{}  []  supposing  \mforall{}x:\mBbbQ{}Cube(k).  (\mneg{}(x  \mmember{}  L))
6.  x  :  \mBbbQ{}Cube(k)
7.  (x  \mmember{}  \mpartial{}(\mpartial{}(K)))
\mvdash{}  False


By

---

Latex:
((InstLemma  `member-rat-complex-boundary-n`  [\mkleeneopen{}n  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  RepUR  ``in-complex-boundary``  -1
  THEN  D  -1)

---

Home Index