---

Step * 1 1 2 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))
⊢ ∀x:ℚCube(k). (¬(x ∈ face-complex(k;K)))
BY
{ ((D 0 THENA Auto) THEN (RWO "member-face-complex" 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)
⊢ ¬(∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ (x ∈ rat-cube-faces(k;c))))

2
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). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ (x ∈ rat-cube-faces(k;c)))) ⇒ False
⊢ face-complex(k;K) ∈ ℚCube(k) List

---

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))
\mvdash{}  \mforall{}x:\mBbbQ{}Cube(k).  (\mneg{}(x  \mmember{}  face-complex(k;K)))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWO  "member-face-complex"  0  THENA  Auto))

---

Home Index