---

Step * 2 2 1 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. ↑isOdd(||filter(λc.is-rat-cube-face(k;x;c);∂(K))||)
8. dim(x) = (n - 1 - 1) ∈ ℤ
⊢ False
BY
{ ((InstLemma `count-related-pairs` [⌜ℚCube(k)⌝;⌜ℚCube(k)⌝;⌜K⌝;⌜filter(λv.is-rat-cube-face(k;x;v);face-complex(k;K))⌝;
    ⌜λc,v. is-rat-cube-face(k;v;c)⌝]⋅
    THENA Auto
    )
   THEN Reduce -1
   THEN (InstLemma `lsum-split` [⌜ℚCube(k)⌝;⌜filter(λv.is-rat-cube-face(k;x;v);face-complex(k;K))⌝;
         ⌜λ2f.in-complex-boundary(k;f;K)⌝]⋅
         THENA Auto
         )
   THEN (RWO "-1" (-2) THENA Auto)
   THEN Thin (-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) ∈ ℤ
9. Σ(||filter(λv.is-rat-cube-face(k;v;t);filter(λv.is-rat-cube-face(k;x;v);face-complex(k;K)))|| | t ∈ K)
= (Σ(||filter(λt.is-rat-cube-face(k;s;t);K)|| | s ∈ filter(λs.in-complex-boundary(k;s;K);
                                                           filter(λv.is-rat-cube-face(k;x;v);face-complex(k;K))))
  + Σ(||filter(λt.is-rat-cube-face(k;s;t);K)|| | s ∈ filter(λs.(¬bin-complex-boundary(k;s;K));
                                                            filter(λv.is-rat-cube-face(k;x;v);face-complex(k;K)))))
∈ ℤ
⊢ 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.  \muparrow{}isOdd(||filter(\mlambda{}c.is-rat-cube-face(k;x;c);\mpartial{}(K))||)
8.  dim(x)  =  (n  -  1  -  1)
\mvdash{}  False


By

---

Latex:
((InstLemma  `count-related-pairs`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};
    \mkleeneopen{}filter(\mlambda{}v.is-rat-cube-face(k;x;v);face-complex(k;K))\mkleeneclose{};\mkleeneopen{}\mlambda{}c,v.  is-rat-cube-face(k;v;c)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Reduce  -1
  THEN  (InstLemma  `lsum-split`  [\mkleeneopen{}\mBbbQ{}Cube(k)\mkleeneclose{};\mkleeneopen{}filter(\mlambda{}v.is-rat-cube-face(k;x;v);face-complex(k;K))\mkleeneclose{};
              \mkleeneopen{}\mlambda{}\msubtwo{}f.in-complex-boundary(k;f;K)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index