---

Step * of Lemma dM-lift-unique

∀[I,J:fset(ℕ)]. ∀[f:I ⟶ J]. ∀[g:dma-hom(dM(J);dM(I))].
  dM-lift(I;J;f) = g ∈ dma-hom(dM(J);dM(I)) supposing ∀j:names(J). ((g <j>) = (f j) ∈ Point(dM(I)))
BY
{ (Auto THEN All (Unfolds ``names-hom dM_inc dM dM-lift``)) }

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

---

Latex:

---

Latex:
\mforall{}[I,J:fset(\mBbbN{})].  \mforall{}[f:I  {}\mrightarrow{}  J].  \mforall{}[g:dma-hom(dM(J);dM(I))].
    dM-lift(I;J;f)  =  g  supposing  \mforall{}j:names(J).  ((g  <j>)  =  (f  j))


By

---

Latex:
(Auto  THEN  All  (Unfolds  ``names-hom  dM\_inc  dM  dM-lift``))

---

Home Index