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