---

Step * 2 of Lemma dm-neg-is-hom


1. T : Type
2. eq : EqDecider(T)
3. Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
4. deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
5. ∀[f:(T + T) ⟶ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))]
     (λac.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)));f;ac)
      ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));opposite-lattice(free-DeMorgan-lattice(T;eq))))
6. y : T@i
⊢ {{inl y}} ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
BY
{ (RevHypSubst 3 0
   THEN Unfold `free-DeMorgan-lattice` 0
   THEN (RWO "free-dl-point" 0 THENA Auto)
   THEN (Assert inl y ∈ T + T BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  Point(free-DeMorgan-lattice(T;eq))  \msim{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
4.  deq-fset(deq-fset(union-deq(T;T;eq;eq)))
      \mmember{}  EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
5.  \mforall{}[f:(T  +  T)  {}\mrightarrow{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))]
          (\mlambda{}ac.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)));f;ac)
            \mmember{}  Hom(free-dist-lattice(T  +  T;  union-deq(T;T;eq;eq)
                                                            );opposite-lattice(free-DeMorgan-lattice(T;eq))))
6.  y  :  T@i
\mvdash{}  \{\{inl  y\}\}  \mmember{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))


By

---

Latex:
(RevHypSubst  3  0
  THEN  Unfold  `free-DeMorgan-lattice`  0
  THEN  (RWO  "free-dl-point"  0  THENA  Auto)
  THEN  (Assert  inl  y  \mmember{}  T  +  T  BY
                          Auto)
  THEN  Auto)

---

Home Index