---

Step * 1 of Lemma half-cubes-listable


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))))]
BY
{ (D 0 With ⌜[λx.x]⌝  THEN Auto THEN Unfold `rational-cube` 0 THEN FunExt THEN Auto) }

---

Latex:

---

Latex:

1.  c  :  \{c:\mBbbQ{}Cube(0)|  \muparrow{}Inhabited(c)\} 
\mvdash{}  \mexists{}L:\mBbbQ{}Cube(0)  List  [(no\_repeats(\mBbbQ{}Cube(0);L)  \mwedge{}  (\mforall{}h:\mBbbQ{}Cube(0).  ((h  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}is-half-cube(0;h;c))))]


By

---

Latex:
(D  0  With  \mkleeneopen{}[\mlambda{}x.x]\mkleeneclose{}    THEN  Auto  THEN  Unfold  `rational-cube`  0  THEN  FunExt  THEN  Auto)

---

Home Index