---

Step * of Lemma rat-cube-faces_wf

∀[k:ℕ]. ∀[c:ℚCube(k)].  rat-cube-faces(k;c) ∈ {f:ℚCube(k)| f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)}  List supposing ↑Inhabit\000Ced(c)
BY
{ (ProveWfLemma
   THEN MemTypeCD
   THEN Auto
   THEN All Reduce
   THEN (All (RW assert_pushdownC) THENA Auto)
   THEN RWO "lower-rc-face-dimension upper-rc-face-dimension" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[c:\mBbbQ{}Cube(k)].    rat-cube-faces(k;c)  \mmember{}  \{f:\mBbbQ{}Cube(k)|  f  \mleq{}  c  \mwedge{}  (dim(f)  =  (dim(c)  -  1))\}    List  su\000Cpposing  \muparrow{}Inhabited(c)


By

---

Latex:
(ProveWfLemma
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  Reduce
  THEN  (All  (RW  assert\_pushdownC)  THENA  Auto)
  THEN  RWO  "lower-rc-face-dimension  upper-rc-face-dimension"  0
  THEN  Auto)

---

Home Index