Step
*
of Lemma
cube+_interval-0
No Annotations
∀[I:fset(ℕ)]. ∀[i:ℕ].  (cube+(I;i) o [0(𝕀)] = <(i0)> ∈ formal-cube(I) j⟶ formal-cube(I+i))
BY
{ Auto }
1
1. I : fset(ℕ)
2. i : ℕ
⊢ cube+(I;i) o [0(𝕀)] = <(i0)> ∈ formal-cube(I) j⟶ formal-cube(I+i)
Latex:
Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    (cube+(I;i)  o  [0(\mBbbI{})]  =  <(i0)>)
By
Latex:
Auto
Home
Index