Step
*
of Lemma
face-lattice-hom-unique
No Annotations
∀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@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f0 : T ⟶ Point(L)@i
6. f1 : T ⟶ Point(L)@i
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:
No Annotations
\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