---

Step * 2 2 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
{ ((Assert λh,i. if i <z k - 1 then h i else c i fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k) BY
          (((FunExt THENM Reduce 0) THEN Unfold `rational-cube` 0) THEN Auto))
   THEN (D 0 With ⌜map(λh,i. if i <z k - 1 then h i else c i fi ;L)⌝  THENW Auto)
   ) }

1
1. k : ℤ
2. 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. 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 ∈ ℤ)
9. λh,i. if i <z k - 1 then h i else c i fi  ∈ ℚCube(k - 1) ⟶ ℚCube(k)
⊢ no_repeats(ℚCube(k);map(λh,i. if i <z k - 1 then h i else c i fi ;L))
∧ (∀h:ℚCube(k). ((h ∈ map(λh,i. if i <z k - 1 then h i else c i fi ;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.  \mneg{}(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:
((Assert  \mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  c  i  fi    \mmember{}  \mBbbQ{}Cube(k  -  1)  {}\mrightarrow{}  \mBbbQ{}Cube(k)  BY
                (((FunExt  THENM  Reduce  0)  THEN  Unfold  `rational-cube`  0)  THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}map(\mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  c  i  fi  ;L)\mkleeneclose{}    THENW  Auto)
  )

---

Home Index