---

Step * of Lemma dma-lift-compose_wf

∀[I,J,K:Type]. ∀[eqi:EqDecider(I)]. ∀[eqj:EqDecider(J)]. ∀[f:J ⟶ Point(free-DeMorgan-algebra(I;eqi))].
∀[g:K ⟶ Point(free-DeMorgan-algebra(J;eqj))].
  (dma-lift-compose(I;J;eqi;eqj;f;g) ∈ K ⟶ Point(free-DeMorgan-algebra(I;eqi)))
BY
{ Auto }

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))
⊢ dma-lift-compose(I;J;eqi;eqj;f;g) ∈ K ⟶ Point(free-DeMorgan-algebra(I;eqi))

---

Latex:

---

Latex:
\mforall{}[I,J,K:Type].  \mforall{}[eqi:EqDecider(I)].  \mforall{}[eqj:EqDecider(J)].
\mforall{}[f:J  {}\mrightarrow{}  Point(free-DeMorgan-algebra(I;eqi))].  \mforall{}[g:K  {}\mrightarrow{}  Point(free-DeMorgan-algebra(J;eqj))].
    (dma-lift-compose(I;J;eqi;eqj;f;g)  \mmember{}  K  {}\mrightarrow{}  Point(free-DeMorgan-algebra(I;eqi)))


By

---

Latex:
Auto

---

Home Index