Nuprl Definition : constrained-antichain-lattice
constrained-antichain-lattice(T;eq;P) ==
{points={ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} ;
meet=λac1,ac2. glb(P;ac1;ac2);
join=λac1,ac2. lub(P;ac1;ac2);
0={};
1={{}}}
Definitions occuring in Statement :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
fset-constrained-ac-glb: glb(P;ac1;ac2),
fset-constrained-ac-lub: lub(P;ac1;ac2),
fset-antichain: fset-antichain(eq;ac),
fset-all: fset-all(s;x.P[x]),
empty-fset: {},
fset-singleton: {x},
fset: fset(T),
assert: ↑b,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice,
set: {x:A| B[x]} ,
fset: fset(T),
and: P ∧ Q,
assert: ↑b,
fset-antichain: fset-antichain(eq;ac),
fset-all: fset-all(s;x.P[x]),
apply: f a,
fset-constrained-ac-glb: glb(P;ac1;ac2),
lambda: λx.A[x],
fset-constrained-ac-lub: lub(P;ac1;ac2),
fset-singleton: {x},
empty-fset: {}
FDL editor aliases :
constrained-antichain-lattice
Latex:
constrained-antichain-lattice(T;eq;P) ==
\{points=\{ac:fset(fset(T))| (\muparrow{}fset-antichain(eq;ac)) \mwedge{} fset-all(ac;x.P x)\} ;
meet=\mlambda{}ac1,ac2. glb(P;ac1;ac2);
join=\mlambda{}ac1,ac2. lub(P;ac1;ac2);
0=\{\};
1=\{\{\}\}\}
Date html generated:
2020_05_20-AM-08_47_46
Last ObjectModification:
2015_10_06-PM-06_52_15
Theory : lattices
Home
Index