---

Step * of Lemma length-rat-cube-faces

No Annotations
∀k:ℕ. ∀c:ℚCube(k).  ((↑Inhabited(c)) ⇒ (||rat-cube-faces(k;c)|| = (2 * dim(c)) ∈ ℤ))
BY
{ (Auto
   THEN RepUR ``rat-cube-faces mapfilter`` 0
   THEN (RWO  "length-concat" 0 THENA Auto)
   THEN (RWO "map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Fold `lsum` 0) }

1
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
⊢ Σ(2 | x ∈ filter(λj.(dim(c j) =z 1);upto(k))) = (2 * dim(c)) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).    ((\muparrow{}Inhabited(c))  {}\mRightarrow{}  (||rat-cube-faces(k;c)||  =  (2  *  dim(c))))


By

---

Latex:
(Auto
  THEN  RepUR  ``rat-cube-faces  mapfilter``  0
  THEN  (RWO    "length-concat"  0  THENA  Auto)
  THEN  (RWO  "map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Fold  `lsum`  0)

---

Home Index