---

Step * of Lemma cube+_wf

No Annotations
∀[I:fset(ℕ)]. ∀[i:ℕ].  (cube+(I;i) ∈ formal-cube(I).𝕀 j⟶ formal-cube(I+i))
BY
{ Intros }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    (cube+(I;i)  \mmember{}  formal-cube(I).\mBbbI{}  j{}\mrightarrow{}  formal-cube(I+i))


By

---

Latex:
Intros

---

Home Index