---

Step * of Lemma half-cubes-listable-ext

∀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
{ Extract of Obid: half-cubes-listable
  not unfolding  primrec lt_int rat-interval-dimension map append qavg q_less qeq q_le
  finishing with (Auto THEN Fold `half-cubes` 0 THEN Auto)
  normalizes to:
  
  λk.half-cubes(k) }

---

Latex:

---

Latex:
\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:
Extract  of  Obid:  half-cubes-listable
not  unfolding    primrec  lt\_int  rat-interval-dimension  map  append  qavg  q\_less  qeq  q\_le
finishing  with  (Auto  THEN  Fold  `half-cubes`  0  THEN  Auto)
normalizes  to:

\mlambda{}k.half-cubes(k)

---

Home Index