---

Step * of Lemma fl-morph-fl1

∀[J,I:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[x:names(I)].  (((x=1))<f> = dM-to-FL(J;f x) ∈ Point(face_lattice(J)))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[J,I:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].  \mforall{}[x:names(I)].    (((x=1))<f>  =  dM-to-FL(J;f  x))


By

---

Latex:
Auto

---

Home Index