---

Step * 1 1 of Lemma dm-neg-opp


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)))
BY
{ Assert ⌜λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}} ∈ (T + T) ⟶ Point(free-DeMorgan-lattice(T;eq))⌝⋅ }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. i : T
⊢ λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}} ∈ (T + T) ⟶ Point(free-DeMorgan-lattice(T;eq))

2
1. T : Type
2. eq : EqDecider(T)
3. i : T
4. λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}} ∈ (T + T) ⟶ Point(free-DeMorgan-lattice(T;eq))
⊢ 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{}  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)));\mlambda{}z.case  z
                                                                                                                            of  inl(a)  =>
                                                                                                                            \{\{inr  a  \}\}
                                                                                                                            |  inr(a)  =>
                                                                                                                            \{\{inl  a\}\};ə-i>)
=  <i>


By

---

Latex:
Assert  \mkleeneopen{}\mlambda{}z.case  z  of  inl(a)  =>  \{\{inr  a  \}\}  |  inr(a)  =>  \{\{inl  a\}\}  \mmember{}  (T  +  T)
                {}\mrightarrow{}  Point(free-DeMorgan-lattice(T;eq))\mkleeneclose{}\mcdot{}

---

Home Index