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