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