---

Step * 2 1 of Lemma half-cubes-listable


1. k : ℤ
2. [%1] : 0 < k
3. c : {c:ℚCube(k)| ↑Inhabited(c)} 
4. ℚCube(k) ⊆r ℚCube(k - 1)
5. {c:ℚCube(k)| ↑Inhabited(c)}  ⊆r {c:ℚCube(k - 1)| ↑Inhabited(c)} 
6. L : ℚCube(k - 1) List
7. [%5] : no_repeats(ℚCube(k - 1);L) ∧ (∀h:ℚCube(k - 1). ((h ∈ L) ⇐⇒ ↑is-half-cube(k - 1;h;c)))
8. dim(c (k - 1)) = 1 ∈ ℤ
⊢ ∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))]
BY
{ (MoveToConcl (-1)
   THEN (GenConclTerm ⌜c (k - 1)⌝⋅ THENA Auto)
   THEN D -2
   THEN RepUR ``rat-interval-dimension`` 0
   THEN AutoSplit
   THEN (D 0 THENA Auto)
   THEN Thin (-1)) }

1
1. k : ℤ
2. [%1] : 0 < k
3. c : {c:ℚCube(k)| ↑Inhabited(c)} 
4. ℚCube(k) ⊆r ℚCube(k - 1)
5. {c:ℚCube(k)| ↑Inhabited(c)}  ⊆r {c:ℚCube(k - 1)| ↑Inhabited(c)} 
6. L : ℚCube(k - 1) List
7. [%5] : no_repeats(ℚCube(k - 1);L) ∧ (∀h:ℚCube(k - 1). ((h ∈ L) ⇐⇒ ↑is-half-cube(k - 1;h;c)))
8. v1 : ℚ
9. v2 : ℚ
10. (c (k - 1)) = <v1, v2> ∈ ℚInterval
11. v1 < v2
⊢ ∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))]

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  0  <  k
3.  c  :  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\} 
4.  \mBbbQ{}Cube(k)  \msubseteq{}r  \mBbbQ{}Cube(k  -  1)
5.  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    \msubseteq{}r  \{c:\mBbbQ{}Cube(k  -  1)|  \muparrow{}Inhabited(c)\} 
6.  L  :  \mBbbQ{}Cube(k  -  1)  List
7.  [\%5]  :  no\_repeats(\mBbbQ{}Cube(k  -  1);L)  \mwedge{}  (\mforall{}h:\mBbbQ{}Cube(k  -  1).  ((h  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(k  -  1;h;c)))
8.  dim(c  (k  -  1))  =  1
\mvdash{}  \mexists{}L:\mBbbQ{}Cube(k)  List  [(no\_repeats(\mBbbQ{}Cube(k);L)  \mwedge{}  (\mforall{}h:\mBbbQ{}Cube(k).  ((h  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(k;h;c))))]


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}c  (k  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  RepUR  ``rat-interval-dimension``  0
  THEN  AutoSplit
  THEN  (D  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index