Nuprl Definition : face-lattice
face-lattice(T;eq) == free-dist-lattice-with-constraints(T + T;union-deq(T;T;eq;eq);x.face-lattice-constraints(x))
Definitions occuring in Statement :
face-lattice-constraints: face-lattice-constraints(x)
,
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x])
,
union-deq: union-deq(A;B;a;b)
,
union: left + right
Definitions occuring in definition :
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x])
,
union: left + right
,
union-deq: union-deq(A;B;a;b)
,
face-lattice-constraints: face-lattice-constraints(x)
FDL editor aliases :
face-lattice
Latex:
face-lattice(T;eq) ==
free-dist-lattice-with-constraints(T + T;union-deq(T;T;eq;eq);x.face-lattice-constraints(x))
Date html generated:
2020_05_20-AM-08_50_38
Last ObjectModification:
2015_10_09-PM-06_43_21
Theory : lattices
Home
Index