---

Step * 1 of Lemma free-dma-lift-unique


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)
BY
{ (UsingVars [`f';`eq2'] (BLemma_o (ioid Obid: free-DeMorgan-algebra-hom-unique))⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  DeMorganAlgebra
4.  eq2  :  EqDecider(Point(dm))
5.  f  :  T  {}\mrightarrow{}  Point(dm)
6.  g  :  dma-hom(free-DeMorgan-algebra(T;eq);dm)
7.  \mforall{}i:T.  ((g  <i>)  =  (f  i))
\mvdash{}  free-dma-lift(T;eq;dm;eq2;f)  =  g


By

---

Latex:
(UsingVars  [`f';`eq2']  (BLemma\_o  (ioid  Obid:  free-DeMorgan-algebra-hom-unique))\mcdot{}  THEN  Auto)

---

Home Index