---

Step * of Lemma face-lattice-property

No Annotations
∀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 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
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. x : T + T
9. c : fset(T + T)
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
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.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
⊢ (g (x=0)) = (f0 x) ∈ 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.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
11. (g (x=0)) = (f0 x) ∈ Point(L)
⊢ (g (x=1)) = (f1 x) ∈ Point(L)

---

Latex:

---

Latex:
No  Annotations
\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  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