Nuprl Definition : rat-cube-faces
rat-cube-faces(k;c) == concat(mapfilter(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];λj.(dim(c j) =z 1);upto(k)))
Definitions occuring in Statement :
upper-rc-face: upper-rc-face(c;j),
lower-rc-face: lower-rc-face(c;j),
rat-interval-dimension: dim(I),
upto: upto(n),
mapfilter: mapfilter(f;P;L),
concat: concat(ll),
cons: [a / b],
nil: [],
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
upto: upto(n),
natural_number: $n,
apply: f a,
rat-interval-dimension: dim(I),
eq_int: (i =z j),
lambda: λx.A[x],
nil: [],
upper-rc-face: upper-rc-face(c;j),
cons: [a / b],
lower-rc-face: lower-rc-face(c;j),
mapfilter: mapfilter(f;P;L),
concat: concat(ll)
FDL editor aliases :
rat-cube-faces
Latex:
rat-cube-faces(k;c) ==
concat(mapfilter(\mlambda{}j.[lower-rc-face(c;j); upper-rc-face(c;j)];\mlambda{}j.(dim(c j) =\msubz{} 1);upto(k)))
Date html generated:
2019_10_29-AM-07_57_07
Last ObjectModification:
2019_10_17-PM-05_22_54
Theory : rationals
Home
Index