---

Step * 2 of Lemma interval-presheaf_wf

.....wf..... 
1. ∀x:fset(ℕ). (dM-lift(x;x;1) = (λx.x) ∈ (Point(dM(x)) ⟶ Point(dM(x))))
2. x : fset(ℕ)
3. y : fset(ℕ)
4. z : fset(ℕ)
5. f : y ⟶ x
6. g : z ⟶ y
⊢ dM-lift(z;y;g) o dM-lift(y;x;f) ∈ dma-hom(dM(x);dM(z))
BY
{ (BLemma `compose-dma-hom` THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  \mforall{}x:fset(\mBbbN{}).  (dM-lift(x;x;1)  =  (\mlambda{}x.x))
2.  x  :  fset(\mBbbN{})
3.  y  :  fset(\mBbbN{})
4.  z  :  fset(\mBbbN{})
5.  f  :  y  {}\mrightarrow{}  x
6.  g  :  z  {}\mrightarrow{}  y
\mvdash{}  dM-lift(z;y;g)  o  dM-lift(y;x;f)  \mmember{}  dma-hom(dM(x);dM(z))


By

---

Latex:
(BLemma  `compose-dma-hom`  THEN  Auto)

---

Home Index