---

Step * of Lemma implies-member-rat-cube-faces

∀k:ℕ. ∀c:ℚCube(k).
  ∀f:{f:ℚCube(k)| f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)} . (f ∈ rat-cube-faces(k;c)) supposing ↑Inhabited(c)
BY
{ (Auto
   THEN (Assert f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ) BY
               Auto)
   THEN D -2
   THEN Thin (-2)
   THEN Unfold `rat-cube-faces` 0
   THEN BLemma `member-concat`
   THEN Auto
   THEN (RWO "member-mapfilter" 0 THENA Auto)
   THEN Reduce 0) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. f : ℚCube(k)
5. f ≤ c
6. dim(f) = (dim(c) - 1) ∈ ℤ
⊢ ∃l:ℚCube(k) List
   ((∃y:ℕk. ((y ∈ upto(k)) ∧ ((↑(dim(c y) =z 1)) c∧ (l = [lower-rc-face(c;y); upper-rc-face(c;y)] ∈ (ℚCube(k) List)))))
   ∧ (f ∈ l))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  f  \mleq{}  c  \mwedge{}  (dim(f)  =  (dim(c)  -  1))  BY
                          Auto)
  THEN  D  -2
  THEN  Thin  (-2)
  THEN  Unfold  `rat-cube-faces`  0
  THEN  BLemma  `member-concat`
  THEN  Auto
  THEN  (RWO  "member-mapfilter"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index