---

Step * of Lemma face-lattice-hom-unique

∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
  ∀[g,h:Hom(face-lattice(T;eq);L)].
    g = h ∈ Hom(face-lattice(T;eq);L) 
    supposing (∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L)))
    ∧ (∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L)))
    ∧ (∀x:T. ((g (x=1)) = (h (x=1)) ∈ 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. f0 : T ⟶ Point(L)
6. f1 : T ⟶ Point(L)
7. g : Point(face-lattice(T;eq)) ⟶ Point(L)
8. ∀[a,b:Point(face-lattice(T;eq))].  ((g a ∧ g b = (g a ∧ b) ∈ Point(L)) ∧ (g a ∨ g b = (g a ∨ b) ∈ Point(L)))
9. (g 0) = 0 ∈ Point(L)
10. (g 1) = 1 ∈ Point(L)
11. h : Point(face-lattice(T;eq)) ⟶ Point(L)
12. ∀[a,b:Point(face-lattice(T;eq))].  ((h a ∧ h b = (h a ∧ b) ∈ Point(L)) ∧ (h a ∨ h b = (h a ∨ b) ∈ Point(L)))
13. (h 0) = 0 ∈ Point(L)
14. (h 1) = 1 ∈ Point(L)
15. ∀x:T. (g (x=0) ∧ g (x=1) = 0 ∈ Point(L))
16. ∀x:T. ((g (x=0)) = (h (x=0)) ∈ Point(L))
17. ∀x:T. ((g (x=1)) = (h (x=1)) ∈ Point(L))
⊢ g = h ∈ (Point(face-lattice(T;eq)) ⟶ Point(L))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).
\mforall{}f0,f1:T  {}\mrightarrow{}  Point(L).
    \mforall{}[g,h:Hom(face-lattice(T;eq);L)].
        g  =  h 
        supposing  (\mforall{}x:T.  (g  (x=0)  \mwedge{}  g  (x=1)  =  0))
        \mwedge{}  (\mforall{}x:T.  ((g  (x=0))  =  (h  (x=0))))
        \mwedge{}  (\mforall{}x:T.  ((g  (x=1))  =  (h  (x=1))))


By

---

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

---

Home Index