---

Step * 2 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
12. v : Hom(face-lattice(T;eq);L)
13. ∀x:T. (((v (x=0)) = (f0 x) ∈ Point(L)) ∧ ((v (x=1)) = (f1 x) ∈ Point(L)))
14. 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=0)) = (g (x=0)) ∈ Point(L)
BY
{ (RWO "-2.1 -6.1" 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.  x  :  T
12.  v  :  Hom(face-lattice(T;eq);L)
13.  \mforall{}x:T.  (((v  (x=0))  =  (f0  x))  \mwedge{}  ((v  (x=1))  =  (f1  x)))
14.  fl-lift(T;eq;L;eqL;f0;f1)  =  v
\mvdash{}  (v  (x=0))  =  (g  (x=0))


By

---

Latex:
(RWO  "-2.1  -6.1"  0  THEN  Auto)

---

Home Index