---

Step * of Lemma is-half-cube-sub-cube

No Annotations
∀[k:ℕ]. ∀h,c:ℚCube(k).  (rat-sub-cube(k;h;c)) supposing ((↑is-half-cube(k;h;c)) and (↑Inhabited(c)))
BY
{ ((RWO  "assert-inhabited-rat-cube assert-is-half-cube" 0 THEN Auto)
   THEN UnfoldTopAb 0
   THEN ParallelLast
   THEN D 4 With ⌜i⌝ 
   THEN EAuto 1) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}h,c:\mBbbQ{}Cube(k).    (rat-sub-cube(k;h;c))  supposing  ((\muparrow{}is-half-cube(k;h;c))  and  (\muparrow{}Inhabited(c)))


By

---

Latex:
((RWO    "assert-inhabited-rat-cube  assert-is-half-cube"  0  THEN  Auto)
  THEN  UnfoldTopAb  0
  THEN  ParallelLast
  THEN  D  4  With  \mkleeneopen{}i\mkleeneclose{} 
  THEN  EAuto  1)

---

Home Index