---

Step * of Lemma lattice-hom-fset-join

∀[l1,l2:BoundedLattice]. ∀[eq1:EqDecider(Point(l1))]. ∀[eq2:EqDecider(Point(l2))]. ∀[f:Hom(l1;l2)].
∀[s:fset(Point(l1))].
  ((f \/(s)) = \/(f"(s)) ∈ Point(l2))
BY
{ (Auto THEN QuotientElimForEquality (-1)) }

1
1. l1 : BoundedLattice
2. l2 : BoundedLattice
3. eq1 : EqDecider(Point(l1))
4. eq2 : EqDecider(Point(l2))
5. f : Hom(l1;l2)
6. s : Base
7. s1 : Base
8. s = s1 ∈ (x,y:Point(l1) List//set-equal(Point(l1);x;y))
9. s ∈ Point(l1) List
10. s1 ∈ Point(l1) List
11. set-equal(Point(l1);s;s1)
⊢ (f \/(s)) = \/(f"(s1)) ∈ Point(l2)

---

Latex:

---

Latex:
\mforall{}[l1,l2:BoundedLattice].  \mforall{}[eq1:EqDecider(Point(l1))].  \mforall{}[eq2:EqDecider(Point(l2))].  \mforall{}[f:Hom(l1;l2)].
\mforall{}[s:fset(Point(l1))].
    ((f  \mbackslash{}/(s))  =  \mbackslash{}/(f"(s)))


By

---

Latex:
(Auto  THEN  QuotientElimForEquality  (-1))

---

Home Index