Nuprl Definition : free-dist-lattice-with-constraints
free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ==
constrained-antichain-lattice(T;eq;λs.fset-contains-none(eq;s;x.Cs[x]))
Definitions occuring in Statement :
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P),
fset-contains-none: fset-contains-none(eq;s;x.Cs[x]),
lambda: λx.A[x]
Definitions occuring in definition :
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P),
lambda: λx.A[x],
fset-contains-none: fset-contains-none(eq;s;x.Cs[x])
FDL editor aliases :
free-dlwc
Latex:
free-dist-lattice-with-constraints(T;eq;x.Cs[x]) ==
constrained-antichain-lattice(T;eq;\mlambda{}s.fset-contains-none(eq;s;x.Cs[x]))
Date html generated:
2020_05_20-AM-08_48_12
Last ObjectModification:
2015_10_08-PM-04_15_43
Theory : lattices
Home
Index