---

Step * of Lemma face-lattice-tube_wf

∀[I:fset(ℕ)]. ∀[phi:Point(face_lattice(I))]. ∀[j:ℕ].  (face-lattice-tube(I;phi;j) ∈ Point(face_lattice(I+j)))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[phi:Point(face\_lattice(I))].  \mforall{}[j:\mBbbN{}].
    (face-lattice-tube(I;phi;j)  \mmember{}  Point(face\_lattice(I+j)))


By

---

Latex:
ProveWfLemma

---

Home Index