---

Step * 2 1 of Lemma fl-lift_wf


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. v : ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
         ∃g:{Hom(face-lattice(T;eq);L)| (∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L))))} 
         supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
9. (TERMOF{face-lattice-property:o, 1:l, i:l} T)
= v
∈ (∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f0,f1:T ⟶ Point(L).
     ∃g:{Hom(face-lattice(T;eq);L)| (∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L))))} 
     supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L)))
⊢ v eq L eqL f0 f1 ∈ {g:Hom(face-lattice(T;eq);L)| 
                      ∀x:T. (((g (x=0)) = (f0 x) ∈ Point(L)) ∧ ((g (x=1)) = (f1 x) ∈ Point(L)))} 
BY
{ (Fold `sq_exists` 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.  v  :  \mforall{}eq:EqDecider(T).  \mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).
              \mforall{}f0,f1:T  {}\mrightarrow{}  Point(L).
                  \mexists{}g:\{Hom(face-lattice(T;eq);L)|  (\mforall{}x:T.  (((g  (x=0))  =  (f0  x))  \mwedge{}  ((g  (x=1))  =  (f1  x))))\} 
                  supposing  \mforall{}x:T.  (f0  x  \mwedge{}  f1  x  =  0)
9.  (TERMOF\{face-lattice-property:o,  1:l,  i:l\}  T)  =  v
\mvdash{}  v  eq  L  eqL  f0  f1  \mmember{}  \{g:Hom(face-lattice(T;eq);L)| 
                                            \mforall{}x:T.  (((g  (x=0))  =  (f0  x))  \mwedge{}  ((g  (x=1))  =  (f1  x)))\} 


By

---

Latex:
(Fold  `sq\_exists`  0  THEN  Auto)

---

Home Index