---

Step * 1 1 1 1 2 1 1 2 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. u : Point(l1)
7. v : Point(l1) List
8. (f /\(v)) = /\(f"(v)) ∈ Point(l2)
⊢ /\(f"({u} ⋃ v)) = f u ∧ /\(f"(v)) ∈ Point(l2)
BY
{ (RWW "fset-image-union lattice-fset-meet-union" 0 THEN Auto) }

1
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})) ∧ /\(f"(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{}  /\mbackslash{}(f"(\{u\}  \mcup{}  v))  =  f  u  \mwedge{}  /\mbackslash{}(f"(v))


By

---

Latex:
(RWW  "fset-image-union  lattice-fset-meet-union"  0  THEN  Auto)

---

Home Index