---

Step * 1 1 1 of Lemma dma-lift-compose_wf

.....assertion..... 
1. I : Type
2. J : Type
3. K : Type
4. eqi : EqDecider(I)
5. eqj : EqDecider(J)
6. f : J ⟶ Point(free-DeMorgan-algebra(I;eqi))
7. g : K ⟶ Point(free-DeMorgan-algebra(J;eqj))
⊢ free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f) ∈ Point(free-DeMorgan-algebra(J;eqj))
  ⟶ Point(free-DeMorgan-algebra(I;eqi))
BY
{ DoSubsume }

1
1. I : Type
2. J : Type
3. K : Type
4. eqi : EqDecider(I)
5. eqj : EqDecider(J)
6. f : J ⟶ Point(free-DeMorgan-algebra(I;eqi))
7. g : K ⟶ Point(free-DeMorgan-algebra(J;eqj))
⊢ free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
  ∈ {g:dma-hom(free-DeMorgan-algebra(J;eqj);free-DeMorgan-algebra(I;eqi))| 
     ∀i:J. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))} 

2
1. I : Type
2. J : Type
3. K : Type
4. eqi : EqDecider(I)
5. eqj : EqDecider(J)
6. f : J ⟶ Point(free-DeMorgan-algebra(I;eqi))
7. g : K ⟶ Point(free-DeMorgan-algebra(J;eqj))
8. free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
= free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
∈ {g:dma-hom(free-DeMorgan-algebra(J;eqj);free-DeMorgan-algebra(I;eqi))| 
   ∀i:J. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))} 
⊢ {g:dma-hom(free-DeMorgan-algebra(J;eqj);free-DeMorgan-algebra(I;eqi))| 
   ∀i:J. ((g <i>) = (f i) ∈ Point(free-DeMorgan-algebra(I;eqi)))}  ⊆r (Point(free-DeMorgan-algebra(J;eqj))
    ⟶ Point(free-DeMorgan-algebra(I;eqi)))

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Type
2.  J  :  Type
3.  K  :  Type
4.  eqi  :  EqDecider(I)
5.  eqj  :  EqDecider(J)
6.  f  :  J  {}\mrightarrow{}  Point(free-DeMorgan-algebra(I;eqi))
7.  g  :  K  {}\mrightarrow{}  Point(free-DeMorgan-algebra(J;eqj))
\mvdash{}  free-dma-lift(J;eqj;free-DeMorgan-algebra(I;eqi);free-dml-deq(I;eqi);f)
    \mmember{}  Point(free-DeMorgan-algebra(J;eqj))  {}\mrightarrow{}  Point(free-DeMorgan-algebra(I;eqi))


By

---

Latex:
DoSubsume

---

Home Index