---

Step * of Lemma fl-lift_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  fl-lift(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)))}  
  supposing ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
BY
{ ((Auto THEN Unfold `fl-lift` 0)
   THEN Subst' TERMOF{face-lattice-property:o, 1:l, 1:l} ~ TERMOF{face-lattice-property:o, 1:l, i:l} 0
   ) }

1
.....equality..... 
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, 1:l} ~ TERMOF{face-lattice-property:o, 1:l, i:l}

2
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)))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[eqL:EqDecider(Point(L))].
\mforall{}[f0,f1:T  {}\mrightarrow{}  Point(L)].
    fl-lift(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)))\}   
    supposing  \mforall{}x:T.  (f0  x  \mwedge{}  f1  x  =  0)


By

---

Latex:
((Auto  THEN  Unfold  `fl-lift`  0)
  THEN  Subst'  TERMOF\{face-lattice-property:o,  1:l,  1:l\}  \msim{}  TERMOF\{face-lattice-property:o,  1:l,  i:l\}  0
  )

---

Home Index