---

Step * of Lemma cube+_interval-1

No Annotations
∀[I:fset(ℕ)]. ∀[i:ℕ].  (cube+(I;i) o [1(𝕀)] = <(i1)> ∈ formal-cube(I) j⟶ formal-cube(I+i))
BY
{ Auto }

1
1. I : fset(ℕ)
2. i : ℕ
⊢ cube+(I;i) o [1(𝕀)] = <(i1)> ∈ formal-cube(I) j⟶ formal-cube(I+i)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    (cube+(I;i)  o  [1(\mBbbI{})]  =  <(i1)>)


By

---

Latex:
Auto

---

Home Index