---

Step * 2 2 1 of Lemma half-cubes-listable


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)))
BY
{ D 0 }

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

2
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)
⊢ ∀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.  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.  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)
9.  \mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  c  i  fi    \mmember{}  \mBbbQ{}Cube(k  -  1)  {}\mrightarrow{}  \mBbbQ{}Cube(k)
\mvdash{}  no\_repeats(\mBbbQ{}Cube(k);map(\mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  c  i  fi  ;L))
\mwedge{}  (\mforall{}h:\mBbbQ{}Cube(k).  ((h  \mmember{}  map(\mlambda{}h,i.  if  i  <z  k  -  1  then  h  i  else  c  i  fi  ;L))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(k;h;c)))


By

---

Latex:
D  0

---

Home Index