---

Step * 1 1 2 of Lemma dm-neg-opp


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)))
BY
{ (Fold `free-dml-deq` 0
   THEN Unfold `dmopp` 0
   THEN RWO "lattice-extend-dl-inc" 0
   THEN Try ((RWO "opposite-lattice-point" 0 THEN Complete (Auto)))
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  i  :  T
4.  \mlambda{}z.case  z  of  inl(a)  =>  \{\{inr  a  \}\}  |  inr(a)  =>  \{\{inl  a\}\}  \mmember{}  (T  +  T)
      {}\mrightarrow{}  Point(free-DeMorgan-lattice(T;eq))
\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:
(Fold  `free-dml-deq`  0
  THEN  Unfold  `dmopp`  0
  THEN  RWO  "lattice-extend-dl-inc"  0
  THEN  Try  ((RWO  "opposite-lattice-point"  0  THEN  Complete  (Auto)))
  THEN  Auto)

---

Home Index