Step
*
1
of Lemma
dM-lift_wf
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : 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` 0 }
1
1. I : fset(ℕ)
2. J : fset(ℕ)
3. f : 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