Step
*
1
1
1
1
2
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)
6. u : Point(l1)
7. v : Point(l1) List
8. (f \/(v)) = \/(f"(v)) ∈ Point(l2)
⊢ (f u ∨ \/(v)) = \/(f"([u / v])) ∈ Point(l2)
BY
{ (Subst' \/(f"([u / v])) = f u ∨ \/(f"(v)) ∈ Point(l2) 0 THEN Auto) }
1
.....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)
⊢ \/(f"([u / v])) = f u ∨ \/(f"(v)) ∈ 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)
6.  u  :  Point(l1)
7.  v  :  Point(l1)  List
8.  (f  \mbackslash{}/(v))  =  \mbackslash{}/(f"(v))
\mvdash{}  (f  u  \mvee{}  \mbackslash{}/(v))  =  \mbackslash{}/(f"([u  /  v]))
By
Latex:
(Subst'  \mbackslash{}/(f"([u  /  v]))  =  f  u  \mvee{}  \mbackslash{}/(f"(v))  0  THEN  Auto)
Home
Index