---

Step * of Lemma free-dma-lift_wf

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

1
1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
⊢ TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} T eq dm eq2 f ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| 
                                                                      ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} 

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `free-dma-lift`  0)

---

Home Index