---

Step * 2 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))
⊢ TERMOF{face-lattice-property:o, 1:l, i:l} T 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
{ GenConclAtAddr [2;1;1;1;1;1] }

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. ∀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)))} 

---

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)
\mvdash{}  TERMOF\{face-lattice-property:o,  1:l,  i:l\}  T  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:
GenConclAtAddr  [2;1;1;1;1;1]

---

Home Index