---

Step * of Lemma upper-rc-face-dimension

∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk.
  ((↑Inhabited(c)) ⇒ (dim(upper-rc-face(c;j)) = if (dim(c j) =z 0) then dim(c) else dim(c) - 1 fi  ∈ ℤ))
BY
{ ((Auto THEN (Assert ↑Inhabited(c j) BY (RWO "assert-inhabited-rat-cube" 4 THEN Auto)))
   THEN AutoSplit
   THEN RepUR ``rat-cube-dimension`` 0
   THEN (RWO "inhabited-upper-rc-face" 0 THENA Auto)
   THEN AutoSplit
   THEN RepUR ``upper-rc-face`` 0
   THEN (InstLemma `isolate_summand2` [⌜j⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)) }

1
1. k : ℕ
2. c : ℚCube(k)
3. j : ℕk
4. ↑Inhabited(c)
5. ↑Inhabited(c j)
6. dim(c j) = 0 ∈ ℤ
7. ↑Inhabited(c)
8. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = (f[j] + Σ(if (x =z j) then 0 else f[x] fi  | x < n)) ∈ ℤ supposing j < n
⊢ (dim([snd((c j))]) + Σ(if (i =z j) then 0 else dim(if (i =z j) then [snd((c i))] else c i fi ) fi  | i < k))
= (dim(c j) + Σ(if (i =z j) then 0 else dim(c i) fi  | i < k))
∈ ℤ

2
1. k : ℕ
2. c : ℚCube(k)
3. j : ℕk
4. dim(c j) ≠ 0
5. ↑Inhabited(c)
6. ↑Inhabited(c j)
7. ↑Inhabited(c)
8. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = (f[j] + Σ(if (x =z j) then 0 else f[x] fi  | x < n)) ∈ ℤ supposing j < n
⊢ (dim([snd((c j))]) + Σ(if (i =z j) then 0 else dim(if (i =z j) then [snd((c i))] else c i fi ) fi  | i < k))
= ((dim(c j) + Σ(if (i =z j) then 0 else dim(c i) fi  | i < k)) - 1)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).  \mforall{}j:\mBbbN{}k.
    ((\muparrow{}Inhabited(c))
    {}\mRightarrow{}  (dim(upper-rc-face(c;j))  =  if  (dim(c  j)  =\msubz{}  0)  then  dim(c)  else  dim(c)  -  1  fi  ))


By

---

Latex:
((Auto  THEN  (Assert  \muparrow{}Inhabited(c  j)  BY  (RWO  "assert-inhabited-rat-cube"  4  THEN  Auto)))
  THEN  AutoSplit
  THEN  RepUR  ``rat-cube-dimension``  0
  THEN  (RWO  "inhabited-upper-rc-face"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RepUR  ``upper-rc-face``  0
  THEN  (InstLemma  `isolate\_summand2`  [\mkleeneopen{}j\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto))

---

Home Index