---

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

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))].
∀[g,h:Hom(free-dist-lattice(T; eq);L)].
  g = h ∈ Hom(free-dist-lattice(T; eq);L) supposing ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
BY
{ (Auto THEN RepeatFor 2 ((DVar `g' THEN DVar `h' THEN EqTypeCD THEN Auto))) }

1
1. T : Type
2. eq : EqDecider(T)
3. L : BoundedDistributiveLattice
4. eqL : EqDecider(Point(L))
5. g : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
6. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
7. (g 0) = 0 ∈ Point(L)
8. (g 1) = 1 ∈ Point(L)
9. h : Point(free-dist-lattice(T; eq)) ⟶ Point(L)
10. ∀[a,b:Point(free-dist-lattice(T; eq))].  ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
11. (h 0) = 0 ∈ Point(L)
12. (h 1) = 1 ∈ Point(L)
13. ∀x:T. ((g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L))
⊢ g = h ∈ (Point(free-dist-lattice(T; eq)) ⟶ Point(L))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[eqL:EqDecider(Point(L))].
\mforall{}[g,h:Hom(free-dist-lattice(T;  eq);L)].
    g  =  h  supposing  \mforall{}x:T.  ((g  free-dl-inc(x))  =  (h  free-dl-inc(x)))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((DVar  `g'  THEN  DVar  `h'  THEN  EqTypeCD  THEN  Auto)))

---

Home Index