---

Step * 3 of Lemma fl-lift-unique


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. ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
8. g : Hom(face-lattice(T;eq);L)
9. ∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))
10. ∀x:T. (fl-lift(T;eq;L;eqL;f0;f1) (x=0) ∧ fl-lift(T;eq;L;eqL;f0;f1) (x=1) = 0 ∈ Point(L))
11. ∀x:T. ((fl-lift(T;eq;L;eqL;f0;f1) (x=0)) = (g (x=0)) ∈ Point(L))
12. x : T
13. v : Hom(face-lattice(T;eq);L)
14. ∀x:T. (((v (x=0)) = (f0 x) ∈ Point(L)) ∧ ((v (x=1)) = (f1 x) ∈ Point(L)))
15. fl-lift(T;eq;L;eqL;f0;f1)
= v
∈ {g:Hom(face-lattice(T;eq);L)| ∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))} 
⊢ (v (x=1)) = (g (x=1)) ∈ Point(L)
BY
{ (RWO "-2.2 -7.2" 0 THEN Auto) }

---

Latex:

---

Latex:

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.  \mforall{}x:T.  (f0  x  \mwedge{}  f1  x  =  0)
8.  g  :  Hom(face-lattice(T;eq);L)
9.  \mforall{}x:T.  (((g  (x=0))  =  (f0  x))  \mwedge{}  ((g  (x=1))  =  (f1  x)))
10.  \mforall{}x:T.  (fl-lift(T;eq;L;eqL;f0;f1)  (x=0)  \mwedge{}  fl-lift(T;eq;L;eqL;f0;f1)  (x=1)  =  0)
11.  \mforall{}x:T.  ((fl-lift(T;eq;L;eqL;f0;f1)  (x=0))  =  (g  (x=0)))
12.  x  :  T
13.  v  :  Hom(face-lattice(T;eq);L)
14.  \mforall{}x:T.  (((v  (x=0))  =  (f0  x))  \mwedge{}  ((v  (x=1))  =  (f1  x)))
15.  fl-lift(T;eq;L;eqL;f0;f1)  =  v
\mvdash{}  (v  (x=1))  =  (g  (x=1))


By

---

Latex:
(RWO  "-2.2  -7.2"  0  THEN  Auto)

---

Home Index