Nuprl Definition : lattice-hom
Hom(l1;l2) ==
{f:Point(l1) ⟶ Point(l2)|
∀[a,b:Point(l1)]. ((f a ∧ f b = (f a ∧ b) ∈ Point(l2)) ∧ (f a ∨ f b = (f a ∨ b) ∈ Point(l2)))}
Definitions occuring in Statement :
lattice-join: a ∨ b,
lattice-meet: a ∧ b,
lattice-point: Point(l),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
uall: ∀[x:A]. B[x],
and: P ∧ Q,
lattice-meet: a ∧ b,
equal: s = t ∈ T,
lattice-point: Point(l),
apply: f a,
lattice-join: a ∨ b
FDL editor aliases :
lattice-hom
Latex:
Hom(l1;l2) ==
\{f:Point(l1) {}\mrightarrow{} Point(l2)|
\mforall{}[a,b:Point(l1)]. ((f a \mwedge{} f b = (f a \mwedge{} b)) \mwedge{} (f a \mvee{} f b = (f a \mvee{} b)))\}
Date html generated:
2020_05_20-AM-08_23_47
Last ObjectModification:
2015_10_06-PM-01_45_56
Theory : lattices
Home
Index