---

Step * of Lemma cube+-

No Annotations
∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ].
  (cube-(I;i) o cube+(I;i) = 1(formal-cube(I).𝕀) ∈ formal-cube(I).𝕀 j⟶ formal-cube(I).𝕀)
BY
{ (Intros
   THEN ((CsmEqual THENW Auto) THEN Thin (-1))
   THEN RepeatFor 2 ((FunExt THENA Auto))
   THEN RepUR ``cube-context-adjoin formal-cube`` -1
   THEN D -1
   THEN RepUR ``csm-comp compose cube- cube+ csm-id cube-context-adjoin formal-cube`` 0
   THEN (RWO "interval-type-at" 0 THENA Auto)) }

1
1. I : fset(ℕ)
2. i : {i:ℕ| ¬i ∈ I} 
3. I1 : fset(ℕ)
4. alpha : I1 ⟶ I
5. x1 : 𝕀(alpha)
⊢ <λj.if (j =z i) then x1 else alpha j fi , if (i =z i) then x1 else alpha i fi > = <alpha, x1> ∈ (alpha:I1 ⟶ I × 𝕀(I1)\000C)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].    (cube-(I;i)  o  cube+(I;i)  =  1(formal-cube(I).\mBbbI{}))


By

---

Latex:
(Intros
  THEN  ((CsmEqual  THENW  Auto)  THEN  Thin  (-1))
  THEN  RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  RepUR  ``cube-context-adjoin  formal-cube``  -1
  THEN  D  -1
  THEN  RepUR  ``csm-comp  compose  cube-  cube+  csm-id  cube-context-adjoin  formal-cube``  0
  THEN  (RWO  "interval-type-at"  0  THENA  Auto))

---

Home Index