Nuprl Definition : bounded-lattice-hom
Hom(l1;l2) == {f:Hom(l1;l2)| ((f 0) = 0 ∈ Point(l2)) ∧ ((f 1) = 1 ∈ Point(l2))}
Definitions occuring in Statement :
lattice-0: 0,
lattice-1: 1,
lattice-hom: Hom(l1;l2),
lattice-point: Point(l),
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
lattice-hom: Hom(l1;l2),
and: P ∧ Q,
lattice-0: 0,
equal: s = t ∈ T,
lattice-point: Point(l),
apply: f a,
lattice-1: 1
FDL editor aliases :
bounded-lattice-hom
Latex:
Hom(l1;l2) == \{f:Hom(l1;l2)| ((f 0) = 0) \mwedge{} ((f 1) = 1)\}
Date html generated:
2020_05_20-AM-08_24_49
Last ObjectModification:
2015_10_06-PM-01_45_35
Theory : lattices
Home
Index