---

Step * 1 1 1 1 2 1 1 of Lemma fl-morph-comp


1. J : fset(ℕ)
2. K : fset(ℕ)
3. g : K ⟶ J
4. z : Point(dM(J))
5. v : dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);dM(K))
6. ∀i:names(J). ((v <i>) = (g i) ∈ Point(dM(K)))
⊢ (dM-to-FL(J;z))<g> = dM-to-FL(K;v z) ∈ Point(face_lattice(K))
BY
{ (All (Folds ``dM dM_inc``) THEN BLemma `fl-morph-comp-1` THEN Auto) }

---

Latex:

---

Latex:

1.  J  :  fset(\mBbbN{})
2.  K  :  fset(\mBbbN{})
3.  g  :  K  {}\mrightarrow{}  J
4.  z  :  Point(dM(J))
5.  v  :  dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);dM(K))
6.  \mforall{}i:names(J).  ((v  <i>)  =  (g  i))
\mvdash{}  (dM-to-FL(J;z))<g>  =  dM-to-FL(K;v  z)


By

---

Latex:
(All  (Folds  ``dM  dM\_inc``)  THEN  BLemma  `fl-morph-comp-1`  THEN  Auto)

---

Home Index