Nuprl Definition : set-ss
{x:ss | P[x]} == Point={x:Point(ss)| P[x]} #=λx,y. x # y cotrans=ss."#or"
Definitions occuring in Statement :
mk-ss: Point=P #=Sep cotrans=C,
ss-sep: x # y,
ss-point: Point(ss),
set: {x:A| B[x]} ,
lambda: λx.A[x],
token: "$token",
record-select: r.x
Definitions occuring in definition :
mk-ss: Point=P #=Sep cotrans=C,
set: {x:A| B[x]} ,
ss-point: Point(ss),
lambda: λx.A[x],
ss-sep: x # y,
record-select: r.x,
token: "$token"
FDL editor aliases :
set-ss
Latex:
\{x:ss | P[x]\} == Point=\{x:Point(ss)| P[x]\} \#=\mlambda{}x,y. x \# y cotrans=ss."\#or"
Date html generated:
2019_10_31-AM-07_26_49
Last ObjectModification:
2019_09_19-PM-04_09_55
Theory : constructive!algebra
Home
Index