---

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


1. l1 : BoundedLattice
2. l2 : BoundedLattice
3. eq1 : EqDecider(Point(l1))
4. eq2 : EqDecider(Point(l2))
5. f : Hom(l1;l2)
⊢ (f \/([])) = \/(f"([])) ∈ Point(l2)
BY
{ (Subst' f"([]) ~ [] 0 THENA Auto) }

1
1. l1 : BoundedLattice
2. l2 : BoundedLattice
3. eq1 : EqDecider(Point(l1))
4. eq2 : EqDecider(Point(l2))
5. f : Hom(l1;l2)
⊢ (f \/([])) = \/([]) ∈ Point(l2)

---

Latex:

---

Latex:

1.  l1  :  BoundedLattice
2.  l2  :  BoundedLattice
3.  eq1  :  EqDecider(Point(l1))
4.  eq2  :  EqDecider(Point(l2))
5.  f  :  Hom(l1;l2)
\mvdash{}  (f  \mbackslash{}/([]))  =  \mbackslash{}/(f"([]))


By

---

Latex:
(Subst'  f"([])  \msim{}  []  0  THENA  Auto)

---

Home Index