---

Step * 1 1 of Lemma dM-hom-unique


1. I : fset(ℕ)
2. L : BoundedDistributiveLattice
3. eqL : EqDecider(Point(L))
4. g : Hom(free-DeMorgan-algebra(names(I);NamesDeq);L)
5. h : Hom(free-DeMorgan-algebra(names(I);NamesDeq);L)
6. ∀i:names(I). (((g <i>) = (h <i>) ∈ Point(L)) ∧ ((g <1-i>) = (h <1-i>) ∈ Point(L)))
7. ∀[g,h:Hom(free-DeMorgan-lattice(names(I);NamesDeq);L)].
     g = h ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);L) 
     supposing ∀x:names(I) + names(I). ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
8. Hom(free-DeMorgan-lattice(names(I);NamesDeq);L) = Hom(free-DeMorgan-algebra(names(I);NamesDeq);L) ∈ Type
9. x : names(I) + names(I)
⊢ (g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L)
BY
{ (D -1 THEN Folds ``dminc dmopp`` 0 THEN Folds ``dM_inc dM_opp`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  L  :  BoundedDistributiveLattice
3.  eqL  :  EqDecider(Point(L))
4.  g  :  Hom(free-DeMorgan-algebra(names(I);NamesDeq);L)
5.  h  :  Hom(free-DeMorgan-algebra(names(I);NamesDeq);L)
6.  \mforall{}i:names(I).  (((g  <i>)  =  (h  <i>))  \mwedge{}  ((g  ə-i>)  =  (h  ə-i>)))
7.  \mforall{}[g,h:Hom(free-DeMorgan-lattice(names(I);NamesDeq);L)].
          g  =  h  supposing  \mforall{}x:names(I)  +  names(I).  ((g  free-dl-inc(x))  =  (h  free-dl-inc(x)))
8.  Hom(free-DeMorgan-lattice(names(I);NamesDeq);L)  =  Hom(free-DeMorgan-algebra(names(I);NamesDeq);L)
9.  x  :  names(I)  +  names(I)
\mvdash{}  (g  free-dl-inc(x))  =  (h  free-dl-inc(x))


By

---

Latex:
(D  -1  THEN  Folds  ``dminc  dmopp``  0  THEN  Folds  ``dM\_inc  dM\_opp``  0  THEN  Auto)

---

Home Index