Step * 1 of Lemma dM-lift_wf


1. fset(ℕ)
2. fset(ℕ)
3. names(J) ⟶ Point(dM(I))
⊢ dM-lift(I;J;f) ∈ {g:dma-hom(dM(J);dM(I))| ∀j:names(J). ((g <j>(f j) ∈ Point(dM(I)))} 
BY
Unfold `dM-lift` }

1
1. fset(ℕ)
2. fset(ℕ)
3. names(J) ⟶ Point(dM(I))
⊢ free-dma-lift(names(J);NamesDeq;dM(I);free-dml-deq(names(I);NamesDeq);f) ∈ {g:dma-hom(dM(J);dM(I))| 
                                                                              ∀j:names(J)
                                                                                ((g <j>(f j) ∈ Point(dM(I)))} 


Latex:


Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  f  :  names(J)  {}\mrightarrow{}  Point(dM(I))
\mvdash{}  dM-lift(I;J;f)  \mmember{}  \{g:dma-hom(dM(J);dM(I))|  \mforall{}j:names(J).  ((g  <j>)  =  (f  j))\} 


By


Latex:
Unfold  `dM-lift`  0




Home Index