---

Step * 2 of Lemma half-cubes-listable


1. k : ℤ
2. [%1] : 0 < k
3. ∀c:{c:ℚCube(k - 1)| ↑Inhabited(c)} 
     (∃L:ℚCube(k - 1) List [(no_repeats(ℚCube(k - 1);L) ∧ (∀h:ℚCube(k - 1). ((h ∈ L) ⇐⇒ ↑is-half-cube(k - 1;h;c))))])
4. c : {c:ℚCube(k)| ↑Inhabited(c)} 
⊢ ∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))]
BY
{ ((Assert ℚCube(k) ⊆r ℚCube(k - 1) BY
          (Unfold `rational-cube` 0 THEN Auto))
   THEN (Assert {c:ℚCube(k)| ↑Inhabited(c)}  ⊆r {c:ℚCube(k - 1)| ↑Inhabited(c)}  BY
               ((D 0 THENA Auto)
                THEN D -1
                THEN (RWO "assert-inhabited-rat-cube" (-1) THENA Auto)
                THEN (MemTypeCD THENW Auto)
                THEN RWW "assert-inhabited-rat-cube" 0
                THEN Auto))
   THEN (D 3 With ⌜c⌝  THENA Auto)
   THEN D -1
   THEN ExRepD
   THEN (Decide ⌜dim(c (k - 1)) = 1 ∈ ℤ⌝⋅ THENA Auto)) }

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. 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))))]

2
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))))]

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  [\%1]  :  0  <  k
3.  \mforall{}c:\{c:\mBbbQ{}Cube(k  -  1)|  \muparrow{}Inhabited(c)\} 
          (\mexists{}L:\mBbbQ{}Cube(k  -  1)  List  [(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))))])
4.  c  :  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\} 
\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:
((Assert  \mBbbQ{}Cube(k)  \msubseteq{}r  \mBbbQ{}Cube(k  -  1)  BY
                (Unfold  `rational-cube`  0  THEN  Auto))
  THEN  (Assert  \{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}    \msubseteq{}r  \{c:\mBbbQ{}Cube(k  -  1)|  \muparrow{}Inhabited(c)\}    BY
                          ((D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  (RWO  "assert-inhabited-rat-cube"  (-1)  THENA  Auto)
                            THEN  (MemTypeCD  THENW  Auto)
                            THEN  RWW  "assert-inhabited-rat-cube"  0
                            THEN  Auto))
  THEN  (D  3  With  \mkleeneopen{}c\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  ExRepD
  THEN  (Decide  \mkleeneopen{}dim(c  (k  -  1))  =  1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index