---

Step * of Lemma free-dist-lattice-with-constraints-property

No Annotations
∀[T:Type]
  ∀eq:EqDecider(T)
    ∀[Cs:T ⟶ fset(fset(T))]
      ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
        ∃g:Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L)
         (f = (g o (λx.free-dlwc-inc(eq;a.Cs[a];x))) ∈ (T ⟶ Point(L))) 
        supposing ∀x:T. ∀c:fset(T).  (c ∈ Cs[x] ⇒ (/\(f"(c)) = 0 ∈ Point(L)))
BY
{ (Auto
   THEN With
   ⌜λac.lattice-extend-wc(L;eq;eqL;f;ac)⌝ (D 0)⋅
   THEN Auto
   THEN Try ((FunExt THEN RepUR ``compose`` 0 THEN Auto))
   THEN Try ((BLemma `lattice-extend-is-hom-constrained` THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T)
        \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))]
            \mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).  \mforall{}f:T  {}\mrightarrow{}  Point(L).
                \mexists{}g:Hom(free-dist-lattice-with-constraints(T;eq;x.Cs[x]);L)
                  (f  =  (g  o  (\mlambda{}x.free-dlwc-inc(eq;a.Cs[a];x)))) 
                supposing  \mforall{}x:T.  \mforall{}c:fset(T).    (c  \mmember{}  Cs[x]  {}\mRightarrow{}  (/\mbackslash{}(f"(c))  =  0))


By

---

Latex:
(Auto
  THEN  With
  \mkleeneopen{}\mlambda{}ac.lattice-extend-wc(L;eq;eqL;f;ac)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  ((FunExt  THEN  RepUR  ``compose``  0  THEN  Auto))
  THEN  Try  ((BLemma  `lattice-extend-is-hom-constrained`  THEN  Auto)))

---

Home Index