---

Step * of Lemma dM-hom-unique

∀[I:fset(ℕ)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[g,h:Hom(dM(I);L)].
  g = h ∈ Hom(dM(I);L) supposing ∀i:names(I). (((g <i>) = (h <i>) ∈ Point(L)) ∧ ((g <1-i>) = (h <1-i>) ∈ Point(L)))
BY
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[eqL:EqDecider(Point(L))].  \mforall{}[g,h:Hom(dM(I);L)].
    g  =  h  supposing  \mforall{}i:names(I).  (((g  <i>)  =  (h  <i>))  \mwedge{}  ((g  ə-i>)  =  (h  ə-i>)))


By

---

Latex:
Auto

---

Home Index