---

Step * 1 1 1 1 2 1 1 1 of Lemma lattice-hom-fset-join

.....equality..... 
1. l1 : BoundedLattice
2. l2 : BoundedLattice
3. eq1 : EqDecider(Point(l1))
4. eq2 : EqDecider(Point(l2))
5. f : Hom(l1;l2)
6. u : Point(l1)
7. v : Point(l1) List
8. (f \/(v)) = \/(f"(v)) ∈ Point(l2)
⊢ [u / v] = {u} ⋃ v ∈ fset(Point(l1))
BY
{ (InstLemma `fset-add-as-cons` [⌜Point(l1)⌝;⌜eq1⌝]⋅ THEN Auto) }

1
1. l1 : BoundedLattice
2. l2 : BoundedLattice
3. eq1 : EqDecider(Point(l1))
4. eq2 : EqDecider(Point(l2))
5. f : Hom(l1;l2)
6. u : Point(l1)
7. v : Point(l1) List
8. (f \/(v)) = \/(f"(v)) ∈ Point(l2)
9. ∀[s:fset(Point(l1))]. ∀[x:Point(l1)].  (fset-add(eq1;x;s) = [x / s] ∈ fset(Point(l1)))
⊢ [u / v] = {u} ⋃ v ∈ fset(Point(l1))

---

Latex:

---

Latex:
.....equality..... 
1.  l1  :  BoundedLattice
2.  l2  :  BoundedLattice
3.  eq1  :  EqDecider(Point(l1))
4.  eq2  :  EqDecider(Point(l2))
5.  f  :  Hom(l1;l2)
6.  u  :  Point(l1)
7.  v  :  Point(l1)  List
8.  (f  \mbackslash{}/(v))  =  \mbackslash{}/(f"(v))
\mvdash{}  [u  /  v]  =  \{u\}  \mcup{}  v


By

---

Latex:
(InstLemma  `fset-add-as-cons`  [\mkleeneopen{}Point(l1)\mkleeneclose{};\mkleeneopen{}eq1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index