---

Step * 1 1 2 1 1 1 1 1 1 of Lemma boundary-of-0-dim-is-nil


1. k : ℕ
2. K : ℚCube(k) List
3. (∀c∈K.dim(c) = 0 ∈ ℤ)
4. ∀[L:ℚCube(k) List]. L ~ [] supposing ∀x:ℚCube(k). (¬(x ∈ L))
5. x : ℚCube(k)
6. c : ℚCube(k)
7. (c ∈ K)
8. ↑Inhabited(c)
9. (x ∈ concat(map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k)))))
10. dim(c) = 0 ∈ ℤ
11. ∀[L:ℕk List]. L ~ [] supposing ∀x:ℕk. (¬(x ∈ L))
12. x1 : ℕk
⊢ ¬(x1 ∈ filter(λj.(dim(c j) =z 1);upto(k)))
BY
{ (((RWO "member_filter" 0 THENA Auto) THEN Reduce 0) THEN (D 0 THENA Auto)) }

1
1. k : ℕ
2. K : ℚCube(k) List
3. (∀c∈K.dim(c) = 0 ∈ ℤ)
4. ∀[L:ℚCube(k) List]. L ~ [] supposing ∀x:ℚCube(k). (¬(x ∈ L))
5. x : ℚCube(k)
6. c : ℚCube(k)
7. (c ∈ K)
8. ↑Inhabited(c)
9. (x ∈ concat(map(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];filter(λj.(dim(c j) =z 1);upto(k)))))
10. dim(c) = 0 ∈ ℤ
11. ∀[L:ℕk List]. L ~ [] supposing ∀x:ℕk. (¬(x ∈ L))
12. x1 : ℕk
13. (x1 ∈ upto(k)) ∧ (↑(dim(c x1) =z 1))
⊢ False

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  K  :  \mBbbQ{}Cube(k)  List
3.  (\mforall{}c\mmember{}K.dim(c)  =  0)
4.  \mforall{}[L:\mBbbQ{}Cube(k)  List].  L  \msim{}  []  supposing  \mforall{}x:\mBbbQ{}Cube(k).  (\mneg{}(x  \mmember{}  L))
5.  x  :  \mBbbQ{}Cube(k)
6.  c  :  \mBbbQ{}Cube(k)
7.  (c  \mmember{}  K)
8.  \muparrow{}Inhabited(c)
9.  (x  \mmember{}  concat(map(\mlambda{}j.[lower-rc-face(c;j);  upper-rc-face(c;j)];filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k)))))
10.  dim(c)  =  0
11.  \mforall{}[L:\mBbbN{}k  List].  L  \msim{}  []  supposing  \mforall{}x:\mBbbN{}k.  (\mneg{}(x  \mmember{}  L))
12.  x1  :  \mBbbN{}k
\mvdash{}  \mneg{}(x1  \mmember{}  filter(\mlambda{}j.(dim(c  j)  =\msubz{}  1);upto(k)))


By

---

Latex:
(((RWO  "member\_filter"  0  THENA  Auto)  THEN  Reduce  0)  THEN  (D  0  THENA  Auto))

---

Home Index