---

Step * of Lemma half-cubes-listable

No Annotations
∀k:ℕ. ∀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
{ (InductionOnNat THEN Auto) }

1
1. c : {c:ℚCube(0)| ↑Inhabited(c)} 
⊢ ∃L:ℚCube(0) List [(no_repeats(ℚCube(0);L) ∧ (∀h:ℚCube(0). ((h ∈ L) ⇐⇒ ↑is-half-cube(0;h;c))))]

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}c:\{c:\mBbbQ{}Cube(k)|  \muparrow{}Inhabited(c)\}  .
    (\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:
(InductionOnNat  THEN  Auto)

---

Home Index