Step
*
1
1
of Lemma
lattice-hom-fset-meet
.....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))
BY
{ D 0 }
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"(s)) ∈ 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)
⊢ /\(f"(s)) = /\(f"(s1)) ∈ Point(l2)
Latex:
Latex:
.....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
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"(s))) \mwedge{} (/\mbackslash{}(f"(s)) = /\mbackslash{}(f"(s1)))
By
Latex:
D 0
Home
Index