---

Step * 1 of Lemma dM-lift-unique


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))
BY
{ ((InstLemma `free-dma-lift-unique` [⌜names(J)⌝;⌜NamesDeq⌝;⌜dM(I)⌝;⌜free-dml-deq(names(I);NamesDeq)⌝;⌜f⌝;⌜g⌝]⋅
    THENA Auto
    )
   THEN All (Fold `dM`)
   THEN Try (Trivial)) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  J  :  fset(\mBbbN{})
3.  f  :  names(J)  {}\mrightarrow{}  Point(dM(I))
4.  g  :  dma-hom(free-DeMorgan-algebra(names(J);NamesDeq);free-DeMorgan-algebra(names(I);NamesDeq))
5.  \mforall{}j:names(J).  ((g  <j>)  =  (f  j))
\mvdash{}  free-dma-lift(names(J);NamesDeq;dM(I);free-dml-deq(names(I);NamesDeq);f)  =  g


By

---

Latex:
((InstLemma  `free-dma-lift-unique`  [\mkleeneopen{}names(J)\mkleeneclose{};\mkleeneopen{}NamesDeq\mkleeneclose{};\mkleeneopen{}dM(I)\mkleeneclose{};\mkleeneopen{}free-dml-deq(names(I);NamesDeq)\mkleeneclose{};
    \mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  All  (Fold  `dM`)
  THEN  Try  (Trivial))

---

Home Index