Nuprl Definition : dma-hom
dma-hom(dma1;dma2) == {f:Hom(dma1;dma2)| ∀[a:Point(dma1)]. (¬(f a) = (f ¬(a)) ∈ Point(dma2))}
Definitions occuring in Statement :
dma-neg: ¬(x),
bounded-lattice-hom: Hom(l1;l2),
lattice-point: Point(l),
uall: ∀[x:A]. B[x],
set: {x:A| B[x]} ,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
bounded-lattice-hom: Hom(l1;l2),
uall: ∀[x:A]. B[x],
equal: s = t ∈ T,
lattice-point: Point(l),
apply: f a,
dma-neg: ¬(x)
FDL editor aliases :
dma-hom
Latex:
dma-hom(dma1;dma2) == \{f:Hom(dma1;dma2)| \mforall{}[a:Point(dma1)]. (\mneg{}(f a) = (f \mneg{}(a)))\}
Date html generated:
2016_05_18-AM-11_48_27
Last ObjectModification:
2015_10_12-PM-05_15_47
Theory : lattices
Home
Index