---

Step * 1 of Lemma compose-dma-hom


1. dma1 : DeMorganAlgebra
2. dma2 : DeMorganAlgebra
3. dma3 : DeMorganAlgebra
4. f : Hom(dma1;dma2)
5. ∀[a:Point(dma1)]. (¬(f a) = (f ¬(a)) ∈ Point(dma2))
6. g : Hom(dma2;dma3)
7. ∀[a:Point(dma2)]. (¬(g a) = (g ¬(a)) ∈ Point(dma3))
⊢ g o f ∈ Hom(dma1;dma3)
BY
{ (BLemma `compose-bounded-lattice-hom` THEN Auto) }

---

Latex:

---

Latex:

1.  dma1  :  DeMorganAlgebra
2.  dma2  :  DeMorganAlgebra
3.  dma3  :  DeMorganAlgebra
4.  f  :  Hom(dma1;dma2)
5.  \mforall{}[a:Point(dma1)].  (\mneg{}(f  a)  =  (f  \mneg{}(a)))
6.  g  :  Hom(dma2;dma3)
7.  \mforall{}[a:Point(dma2)].  (\mneg{}(g  a)  =  (g  \mneg{}(a)))
\mvdash{}  g  o  f  \mmember{}  Hom(dma1;dma3)


By

---

Latex:
(BLemma  `compose-bounded-lattice-hom`  THEN  Auto)

---

Home Index