---

Step * 1 of Lemma dM-hom-unique


1. I : fset(ℕ)
2. L : BoundedDistributiveLattice
3. eqL : EqDecider(Point(L))
4. g : Hom(dM(I);L)
5. h : Hom(dM(I);L)
6. ∀i:names(I). (((g <i>) = (h <i>) ∈ Point(L)) ∧ ((g <1-i>) = (h <1-i>) ∈ Point(L)))
⊢ g = h ∈ Hom(dM(I);L)
BY
{ (All (Unfold `dM`)⋅
   THEN (InstLemma `free-dist-lattice-hom-unique2` [⌜names(I) + names(I)⌝;
         ⌜union-deq(names(I);names(I);NamesDeq;NamesDeq)⌝;⌜L⌝;⌜eqL⌝]⋅
         THENA Auto
         )
   THEN Fold `free-DeMorgan-lattice` (-1)
   THEN (InstLemma `free-dma-hom-is-lattice-hom`[⌜names(I)⌝;⌜NamesDeq⌝;⌜L⌝]⋅ THENA Auto)
   THEN InstHyp [⌜g⌝;⌜h⌝] (-2)⋅
   THEN Auto) }

1
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)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  L  :  BoundedDistributiveLattice
3.  eqL  :  EqDecider(Point(L))
4.  g  :  Hom(dM(I);L)
5.  h  :  Hom(dM(I);L)
6.  \mforall{}i:names(I).  (((g  <i>)  =  (h  <i>))  \mwedge{}  ((g  ə-i>)  =  (h  ə-i>)))
\mvdash{}  g  =  h


By

---

Latex:
(All  (Unfold  `dM`)\mcdot{}
  THEN  (InstLemma  `free-dist-lattice-hom-unique2`  [\mkleeneopen{}names(I)  +  names(I)\mkleeneclose{};
              \mkleeneopen{}union-deq(names(I);names(I);NamesDeq;NamesDeq)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `free-DeMorgan-lattice`  (-1)
  THEN  (InstLemma  `free-dma-hom-is-lattice-hom`[\mkleeneopen{}names(I)\mkleeneclose{};\mkleeneopen{}NamesDeq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto)

---

Home Index