---

Step * of Lemma free-dma-lift-unique

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[dm:DeMorganAlgebra]. ∀[eq2:EqDecider(Point(dm))]. ∀[f:T ⟶ Point(dm)].
∀[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
  free-dma-lift(T;eq;dm;eq2;f) = g ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm) 
  supposing ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
6. g : dma-hom(free-DeMorgan-algebra(T;eq);dm)
7. ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
⊢ free-dma-lift(T;eq;dm;eq2;f) = g ∈ dma-hom(free-DeMorgan-algebra(T;eq);dm)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[dm:DeMorganAlgebra].  \mforall{}[eq2:EqDecider(Point(dm))].
\mforall{}[f:T  {}\mrightarrow{}  Point(dm)].  \mforall{}[g:dma-hom(free-DeMorgan-algebra(T;eq);dm)].
    free-dma-lift(T;eq;dm;eq2;f)  =  g  supposing  \mforall{}i:T.  ((g  <i>)  =  (f  i))


By

---

Latex:
Auto

---

Home Index