---

Step * of Lemma dM-hom-basis

∀[I:fset(ℕ)]. ∀[x:Point(dM(I))]. ∀[l:BoundedLattice].
  ∀eq:EqDecider(Point(l)). ∀[h:Hom(dM(I);l)]. ((h x) = \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) ∈ Point(l))
BY
{ (InstLemma `dM-basis` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (ApFunToHypEquands  `Z' ⌜h Z⌝ ⌜Point(l)⌝ 3⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN (RWO "dM-point" 2 THENA Auto)
   THEN D 2
   THEN Assert ⌜h ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)⌝⋅) }

1
.....assertion..... 
1. I : fset(ℕ)
2. x : fset(fset(names(I) + names(I)))
3. ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);x)
4. x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I))
5. l : BoundedLattice
6. eq : EqDecider(Point(l))
7. h : Hom(dM(I);l)
8. (h x) = (h \/(λs./\(λx.free-dl-inc(x)"(s))"(x))) ∈ Point(l)
⊢ h ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)

2
1. I : fset(ℕ)
2. x : fset(fset(names(I) + names(I)))
3. ↑fset-antichain(union-deq(names(I);names(I);NamesDeq;NamesDeq);x)
4. x = \/(λs./\(λx.free-dl-inc(x)"(s))"(x)) ∈ Point(dM(I))
5. l : BoundedLattice
6. eq : EqDecider(Point(l))
7. h : Hom(dM(I);l)
8. (h x) = (h \/(λs./\(λx.free-dl-inc(x)"(s))"(x))) ∈ Point(l)
9. h ∈ Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)
⊢ \/(λs./\(λx.(h free-dl-inc(x))"(s))"(x)) = (h \/(λs./\(λx.free-dl-inc(x)"(s))"(x))) ∈ Point(l)

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[x:Point(dM(I))].  \mforall{}[l:BoundedLattice].
    \mforall{}eq:EqDecider(Point(l)).  \mforall{}[h:Hom(dM(I);l)].  ((h  x)  =  \mbackslash{}/(\mlambda{}s./\mbackslash{}(\mlambda{}x.(h  free-dl-inc(x))"(s))"(x)))


By

---

Latex:
(InstLemma  `dM-basis`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (ApFunToHypEquands    `Z'  \mkleeneopen{}h  Z\mkleeneclose{}  \mkleeneopen{}Point(l)\mkleeneclose{}  3\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  (RWO  "dM-point"  2  THENA  Auto)
  THEN  D  2
  THEN  Assert  \mkleeneopen{}h  \mmember{}  Hom(free-DeMorgan-lattice(names(I);NamesDeq);l)\mkleeneclose{}\mcdot{})

---

Home Index