---

Step * of Lemma fl-morph-comp-1

∀[J,K:fset(ℕ)]. ∀[f:K ⟶ J]. ∀[z:Point(dM(J))]. ∀[h:dma-hom(dM(J);dM(K))].
  (dM-to-FL(J;z))<f> = dM-to-FL(K;h z) ∈ Point(face_lattice(K)) supposing ∀i:names(J). ((h <i>) = (f i) ∈ Point(dM(K)))
BY
{ Auto }

1
1. J : fset(ℕ)
2. K : fset(ℕ)
3. f : K ⟶ J
4. z : Point(dM(J))
5. h : dma-hom(dM(J);dM(K))
6. ∀i:names(J). ((h <i>) = (f i) ∈ Point(dM(K)))
⊢ (dM-to-FL(J;z))<f> = dM-to-FL(K;h z) ∈ Point(face_lattice(K))

---

Latex:

---

Latex:
\mforall{}[J,K:fset(\mBbbN{})].  \mforall{}[f:K  {}\mrightarrow{}  J].  \mforall{}[z:Point(dM(J))].  \mforall{}[h:dma-hom(dM(J);dM(K))].
    (dM-to-FL(J;z))<f>  =  dM-to-FL(K;h  z)  supposing  \mforall{}i:names(J).  ((h  <i>)  =  (f  i))


By

---

Latex:
Auto

---

Home Index