---

Step * 3 1 1 1 1 of Lemma rat-complex-subdiv_wf

.....set predicate..... 
1. k : ℕ
2. n : ℕ
3. K : ℚCube(k) List
4. no_repeats(ℚCube(k);K)
5. (∀c,d∈K.  Compatible(c;d))
6. ∀c:ℚCube(k). ((c ∈ K) ⇒ (dim(c) = n ∈ ℤ))
7. {K ∈ {c:ℚCube(k)| ↑Inhabited(c)}  List}
8. (K)' ∈ ℚCube(k) List
9. no_repeats(ℚCube(k);(K)')
10. (∀c,d∈(K)'.  Compatible(c;d))
11. c : ℚCube(k)
12. a : ℚCube(k)
13. (a ∈ K)
14. ↑is-half-cube(k;c;a)
15. dim(a) = n ∈ ℤ
⊢ ↑Inhabited(a)
BY
{ (Unfold `rat-cube-dimension` -1 THEN SplitOnHypITE -1  THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  K  :  \mBbbQ{}Cube(k)  List
4.  no\_repeats(\mBbbQ{}Cube(k);K)
5.  (\mforall{}c,d\mmember{}K.    Compatible(c;d))
6.  \mforall{}c:\mBbbQ{}Cube(k).  ((c  \mmember{}  K)  {}\mRightarrow{}  (dim(c)  =  n))
7.  \{K  \mmember{}  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    List\}
8.  (K)'  \mmember{}  \mBbbQ{}Cube(k)  List
9.  no\_repeats(\mBbbQ{}Cube(k);(K)')
10.  (\mforall{}c,d\mmember{}(K)'.    Compatible(c;d))
11.  c  :  \mBbbQ{}Cube(k)
12.  a  :  \mBbbQ{}Cube(k)
13.  (a  \mmember{}  K)
14.  \muparrow{}is-half-cube(k;c;a)
15.  dim(a)  =  n
\mvdash{}  \muparrow{}Inhabited(a)


By

---

Latex:
(Unfold  `rat-cube-dimension`  -1  THEN  SplitOnHypITE  -1    THEN  Auto)

---

Home Index