---

Step * of Lemma free-dist-lattice-hom-unique

∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
∀g,h:Hom(free-dist-lattice(T; eq);L).
  ((f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
  ⇒ (f = (h o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
  ⇒ (g = h ∈ Hom(free-dist-lattice(T; eq);L)))
BY
{ (Auto THEN UsingVars [`eqL'] (BLemma `free-dist-lattice-hom-unique2`) THEN Auto) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f : T ⟶ Point(L)@i
6. g : Hom(free-dist-lattice(T; eq);L)@i
7. h : Hom(free-dist-lattice(T; eq);L)@i
8. f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L))@i
9. f = (h o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L))@i
10. x : T@i
⊢ (g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L)

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).
\mforall{}f:T  {}\mrightarrow{}  Point(L).  \mforall{}g,h:Hom(free-dist-lattice(T;  eq);L).
    ((f  =  (g  o  (\mlambda{}x.free-dl-inc(x))))  {}\mRightarrow{}  (f  =  (h  o  (\mlambda{}x.free-dl-inc(x))))  {}\mRightarrow{}  (g  =  h))


By

---

Latex:
(Auto  THEN  UsingVars  [`eqL']  (BLemma  `free-dist-lattice-hom-unique2`)  THEN  Auto)

---

Home Index