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

.....wf..... 
1. : ℕ
2. : ℚCube(k) List
3. (∀c∈K.dim(c) 0 ∈ ℤ)
4. ∀[L:ℚCube(k) List]. [] supposing ∀x:ℚCube(k). (x ∈ L))
⊢ face-complex(k;K) ∈ ℚCube(k) List
BY
ProveWfLemma }


Latex:


Latex:
.....wf..... 
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{}  face-complex(k;K)  \mmember{}  \mBbbQ{}Cube(k)  List


By


Latex:
ProveWfLemma




Home Index