---

Step * of Lemma fl-morph-comp-dM-lift

∀[I,J:fset(ℕ)]. ∀[f:J ⟶ I]. ∀[z:Point(dM(I))].
  ((dM-to-FL(I;z))<f> = dM-to-FL(J;dM-lift(J;I;f) z) ∈ Point(face_lattice(J)))
BY
{ (Auto THEN BLemma `fl-morph-comp-1` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `fl-morph-comp-1`  THEN  Auto)

---

Home Index