---

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


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)
BY
{ Assert ⌜((f /\(s)) = /\(f"(s)) ∈ Point(l2)) ∧ (/\(f"(s)) = /\(f"(s1)) ∈ Point(l2))⌝⋅ }

1
.....assertion..... 
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"(s)) ∈ Point(l2)) ∧ (/\(f"(s)) = /\(f"(s1)) ∈ Point(l2))

2
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)
12. ((f /\(s)) = /\(f"(s)) ∈ Point(l2)) ∧ (/\(f"(s)) = /\(f"(s1)) ∈ Point(l2))
⊢ (f /\(s)) = /\(f"(s1)) ∈ 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.  s  :  Base
7.  s1  :  Base
8.  s  =  s1
9.  s  \mmember{}  Point(l1)  List
10.  s1  \mmember{}  Point(l1)  List
11.  set-equal(Point(l1);s;s1)
\mvdash{}  (f  /\mbackslash{}(s))  =  /\mbackslash{}(f"(s1))


By

---

Latex:
Assert  \mkleeneopen{}((f  /\mbackslash{}(s))  =  /\mbackslash{}(f"(s)))  \mwedge{}  (/\mbackslash{}(f"(s))  =  /\mbackslash{}(f"(s1)))\mkleeneclose{}\mcdot{}

---

Home Index