---

Step * of Lemma free-dl-generators

∀[X:Type]
  ∀L:BoundedDistributiveLattice
    ∀[f,g:Hom(free-dl(X);L)].
      f = g ∈ Hom(free-dl(X);L) supposing ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
BY
{ ((Intro THEN (Assert Point(free-dl(X)) ~ free-dl-type(X) BY (RW  (SubC (TagC (mk_tag_term 100))) 0 THEN Auto)))
   THEN (Assert Point(free-dl(X)) = free-dl-type(X) ∈ Type BY
               (RepUR ``free-dl`` 0 THEN Auto))
   THEN Auto
   THEN RepeatFor 2 ((DVar `f' THENA Auto))
   THEN RepeatFor 2 ((DVar `g' THENA Auto))
   THEN RepeatFor 2 ((EqTypeCD THEN Auto))
   THEN (FunExt THENA Auto)
   THEN ∀h:hyp. RWO "2" h ) }

1
1. X : Type
2. free-dl-type(X) ~ free-dl-type(X)
3. free-dl-type(X) = free-dl-type(X) ∈ Type
4. L : BoundedDistributiveLattice
5. f : free-dl-type(X) ⟶ Point(L)
6. ∀[a,b:free-dl-type(X)].  ((f a ∧ f b = (f a ∧ b) ∈ Point(L)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(L)))
7. (f 0) = 0 ∈ Point(L)
8. (f 1) = 1 ∈ Point(L)
9. g : free-dl-type(X) ⟶ Point(L)
10. ∀[a,b:free-dl-type(X)].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
11. (g 0) = 0 ∈ Point(L)
12. (g 1) = 1 ∈ Point(L)
13. ∀x:X. ((f free-dl-generator(x)) = (g free-dl-generator(x)) ∈ Point(L))
14. x : free-dl-type(X)
⊢ (f x) = (g x) ∈ Point(L)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}L:BoundedDistributiveLattice
        \mforall{}[f,g:Hom(free-dl(X);L)].
            f  =  g  supposing  \mforall{}x:X.  ((f  free-dl-generator(x))  =  (g  free-dl-generator(x)))


By

---

Latex:
((Intro
    THEN  (Assert  Point(free-dl(X))  \msim{}  free-dl-type(X)  BY
                            (RW    (SubC  (TagC  (mk\_tag\_term  100)))  0  THEN  Auto))
    )
  THEN  (Assert  Point(free-dl(X))  =  free-dl-type(X)  BY
                          (RepUR  ``free-dl``  0  THEN  Auto))
  THEN  Auto
  THEN  RepeatFor  2  ((DVar  `f'  THENA  Auto))
  THEN  RepeatFor  2  ((DVar  `g'  THENA  Auto))
  THEN  RepeatFor  2  ((EqTypeCD  THEN  Auto))
  THEN  (FunExt  THENA  Auto)
  THEN  \mforall{}h:hyp.  RWO  "2"  h  )

---

Home Index