---

Step * 1 1 1 1 2 1 2 of Lemma face-lattice-hom-unique

.....subterm..... T:t
2:n
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))
18. y : fset(fset(T + T))
19. (↑fset-antichain(union-deq(T;T;eq;eq);y)) ∧ (∀a:fset(T + T). (a ∈ y ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a)))))
20. y ∈ Point(face-lattice(T;eq))
21. y
= \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ Point(face-lattice(T;eq))
22. BoundedDistributiveLattice ⊆r BoundedLattice
23. ∀x,y:Point(face-lattice(T;eq)).  Dec(x = y ∈ Point(face-lattice(T;eq)))
24. ∀[f:Hom(face-lattice(T;eq);L)]. ∀[s:fset(Point(face-lattice(T;eq)))].  ((f \/(s)) = \/(f"(s)) ∈ Point(L))
⊢ g"(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
= h"(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ fset(Point(L))
BY
{ ((RWO "fset-image-compose" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN EqCD⋅
   THEN Auto
   THEN FunExt
   THEN Auto
   THEN Reduce 0) }

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))
18. y : fset(fset(T + T))
19. ↑fset-antichain(union-deq(T;T;eq;eq);y)
20. ∀a:fset(T + T). (a ∈ y ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
21. y ∈ Point(face-lattice(T;eq))
22. y
= \/(λs./\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
∈ Point(face-lattice(T;eq))
23. BoundedDistributiveLattice ⊆r BoundedLattice
24. ∀x,y:Point(face-lattice(T;eq)).  Dec(x = y ∈ Point(face-lattice(T;eq)))
25. ∀[f:Hom(face-lattice(T;eq);L)]. ∀[s:fset(Point(face-lattice(T;eq)))].  ((f \/(s)) = \/(f"(s)) ∈ Point(L))
26. x : fset(T + T)
⊢ (g /\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(x)))
= (h /\(λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(x)))
∈ Point(L)

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  BoundedDistributiveLattice
4.  eqL  :  EqDecider(Point(L))
5.  f0  :  T  {}\mrightarrow{}  Point(L)
6.  f1  :  T  {}\mrightarrow{}  Point(L)
7.  g  :  Point(face-lattice(T;eq))  {}\mrightarrow{}  Point(L)
8.  \mforall{}[a,b:Point(face-lattice(T;eq))].    ((g  a  \mwedge{}  g  b  =  (g  a  \mwedge{}  b))  \mwedge{}  (g  a  \mvee{}  g  b  =  (g  a  \mvee{}  b)))
9.  (g  0)  =  0
10.  (g  1)  =  1
11.  h  :  Point(face-lattice(T;eq))  {}\mrightarrow{}  Point(L)
12.  \mforall{}[a,b:Point(face-lattice(T;eq))].    ((h  a  \mwedge{}  h  b  =  (h  a  \mwedge{}  b))  \mwedge{}  (h  a  \mvee{}  h  b  =  (h  a  \mvee{}  b)))
13.  (h  0)  =  0
14.  (h  1)  =  1
15.  \mforall{}x:T.  (g  (x=0)  \mwedge{}  g  (x=1)  =  0)
16.  \mforall{}x:T.  ((g  (x=0))  =  (h  (x=0)))
17.  \mforall{}x:T.  ((g  (x=1))  =  (h  (x=1)))
18.  y  :  fset(fset(T  +  T))
19.  (\muparrow{}fset-antichain(union-deq(T;T;eq;eq);y))
\mwedge{}  (\mforall{}a:fset(T  +  T).  (a  \mmember{}  y  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)))))
20.  y  \mmember{}  Point(face-lattice(T;eq))
21.  y  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
22.  BoundedDistributiveLattice  \msubseteq{}r  BoundedLattice
23.  \mforall{}x,y:Point(face-lattice(T;eq)).    Dec(x  =  y)
24.  \mforall{}[f:Hom(face-lattice(T;eq);L)].  \mforall{}[s:fset(Point(face-lattice(T;eq)))].    ((f  \mbackslash{}/(s))  =  \mbackslash{}/(f"(s)))
\mvdash{}  g"(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))
=  h"(\mlambda{}s./\mbackslash{}(\mlambda{}x.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)"(s))"(y))


By

---

Latex:
((RWO  "fset-image-compose"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  EqCD\mcdot{}
  THEN  Auto
  THEN  FunExt
  THEN  Auto
  THEN  Reduce  0)

---

Home Index