---

Step * 1 of Lemma dm-neg-opp


1. T : Type
2. eq : EqDecider(T)
3. i : T
⊢ ¬(<1-i>) = <i> ∈ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))
BY
{ Unfold `dm-neg` 0 }

1
1. T : Type
2. eq : EqDecider(T)
3. i : T
⊢ lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
                 deq-fset(deq-fset(union-deq(T;T;eq;eq)));λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}};<1-i>)
= <i>
∈ Point(free-dist-lattice(T + T; union-deq(T;T;eq;eq)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  i  :  T
\mvdash{}  \mneg{}(ə-i>)  =  <i>


By

---

Latex:
Unfold  `dm-neg`  0

---

Home Index