Nuprl Definition : face-lattice-constraints
face-lattice-constraints(x) == case x of inl(a) => {{inl a,inr a }} | inr(a) => {{inl a,inr a }}
Definitions occuring in Statement :
fset-pair: {a,b},
fset-singleton: {x},
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
fset-singleton: {x},
fset-pair: {a,b},
inl: inl x,
inr: inr x
FDL editor aliases :
face-lattice-constraints
Latex:
face-lattice-constraints(x) == case x of inl(a) => \{\{inl a,inr a \}\} | inr(a) => \{\{inl a,inr a \}\}
Date html generated:
2020_05_20-AM-08_50_32
Last ObjectModification:
2015_10_09-PM-06_41_11
Theory : lattices
Home
Index