---

Step * 3 of Lemma dm-neg-is-hom-opposite

.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. f : Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq))
⊢ ((f 0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ ((f 1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq))) ∈ Type
BY
{ Auto }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  f  :  Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq))
\mvdash{}  ((f  0)  =  0)  \mwedge{}  ((f  1)  =  1)  \mmember{}  Type


By

---

Latex:
Auto

---

Home Index