---

Step * of Lemma face-lattice-property

∀T:Type. ∀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))
BY
{ (Auto
   THEN (InstLemma_o (ioid Obid: free-dist-lattice-with-constraints-property) [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;
         ⌜λ2x.face-lattice-constraints(x)⌝;⌜L⌝;⌜eqL⌝;⌜λx.case x of inl(a) => f0 a | inr(b) => f1 b⌝]⋅
         THENA Auto
         )
   THEN Try ((Fold `face-lattice` (-1) THEN ParallelLast THEN Auto))) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f0 : T ⟶ Point(L)@i
6. f1 : T ⟶ Point(L)@i
7. ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
8. x : T + T@i
9. c : fset(T + T)@i
10. c ∈ face-lattice-constraints(x)
⊢ /\(λx.case x of inl(a) => f0 a | inr(b) => f1 b"(c)) = 0 ∈ Point(L)

2
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f0 : T ⟶ Point(L)@i
6. f1 : T ⟶ Point(L)@i
7. ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
8. g : Hom(face-lattice(T;eq);L)
9. (λx.case x of inl(a) => f0 a | inr(b) => f1 b)
= (g o (λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)))
∈ ((T + T) ⟶ Point(L))
10. x : T@i
⊢ (g (x=0)) = (f0 x) ∈ Point(L)

3
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f0 : T ⟶ Point(L)@i
6. f1 : T ⟶ Point(L)@i
7. ∀x:T. (f0 x ∧ f1 x = 0 ∈ Point(L))
8. g : Hom(face-lattice(T;eq);L)
9. (λx.case x of inl(a) => f0 a | inr(b) => f1 b)
= (g o (λx.free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);x)))
∈ ((T + T) ⟶ Point(L))
10. x : T@i
11. (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).
    \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)


By

---

Latex:
(Auto
  THEN  (InstLemma\_o  (ioid  Obid:  free-dist-lattice-with-constraints-property)  [\mkleeneopen{}T  +  T\mkleeneclose{};
              \mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}eqL\mkleeneclose{};\mkleeneopen{}\mlambda{}x.case  x
                                                                                                                                                              of  inl(a)  =>
                                                                                                                                                              f0  a
                                                                                                                                                              |  inr(b)  =>
                                                                                                                                                              f1  b\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Try  ((Fold  `face-lattice`  (-1)  THEN  ParallelLast  THEN  Auto)))

---

Home Index