---

Step * of Lemma fl-lift-unique

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:BoundedDistributiveLattice]. ∀[eqL:EqDecider(Point(L))]. ∀[f0,f1:T ⟶ Point(L)].
  ∀g:Hom(face-lattice(T;eq);L)
    fl-lift(T;eq;L;eqL;f0;f1) = g ∈ Hom(face-lattice(T;eq);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
{ (Auto
   THEN UsingVars [`f0';`f1';`eqL'] (BLemma_o (ioid Obid: face-lattice-hom-unique))⋅
   THEN Auto
   THEN (GenConclTerm ⌜fl-lift(T;eq;L;eqL;f0;f1)⌝⋅ THEN Auto)
   THEN D -2
   THEN Auto) }

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. 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
11. v : Hom(face-lattice(T;eq);L)
12. ∀x:T. (((v (x=0)) = (f0 x) ∈ Point(L)) ∧ ((v (x=1)) = (f1 x) ∈ Point(L)))
13. 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) ∧ v (x=1) = 0 ∈ Point(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))
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)

3
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. ((fl-lift(T;eq;L;eqL;f0;f1) (x=0)) = (g (x=0)) ∈ Point(L))
12. x : T
13. v : Hom(face-lattice(T;eq);L)
14. ∀x:T. (((v (x=0)) = (f0 x) ∈ Point(L)) ∧ ((v (x=1)) = (f1 x) ∈ Point(L)))
15. 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=1)) = (g (x=1)) ∈ 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)].
    \mforall{}g:Hom(face-lattice(T;eq);L)
        fl-lift(T;eq;L;eqL;f0;f1)  =  g  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:
(Auto
  THEN  UsingVars  [`f0';`f1';`eqL']  (BLemma\_o  (ioid  Obid:  face-lattice-hom-unique))\mcdot{}
  THEN  Auto
  THEN  (GenConclTerm  \mkleeneopen{}fl-lift(T;eq;L;eqL;f0;f1)\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  D  -2
  THEN  Auto)

---

Home Index