---

Step * of Lemma fl-lift-unique2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  ∀g:Hom(face-lattice(T;eq);L)
    ∀x:Point(face-lattice(T;eq)). ((fl-lift(T;eq;L;eqL;f0;f1) x) = (g x) ∈ Point(L)) 
    supposing ∀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
{ (InstLemma `fl-lift-unique` [] THEN RepeatFor 7 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:BoundedDistributiveLattice].  \mforall{}[eqL:EqDecider(Point(L))].
\mforall{}[f0,f1:T  {}\mrightarrow{}  Point(L)].
    \mforall{}g:Hom(face-lattice(T;eq);L)
        \mforall{}x:Point(face-lattice(T;eq)).  ((fl-lift(T;eq;L;eqL;f0;f1)  x)  =  (g  x)) 
        supposing  \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:
(InstLemma  `fl-lift-unique`  []  THEN  RepeatFor  7  (ParallelLast')  THEN  Auto)

---

Home Index