Nuprl Definition : in_spr
(f 
spr(g)) == 
x:
. ((g mklist(x;f)) = 0)
Definitions occuring in Statement :
nat: ,
all: x:A. B[x],
apply: f a,
natural_number: $n,
equal: s = t,
mklist: mklist(n;f)
FDL editor aliases :
in_spr
(f \mmember{} spr(g)) == \mforall{}x:\mBbbN{}. ((g mklist(x;f)) = 0)
Date html generated:
2013_03_20-AM-10_32_36
Last ObjectModification:
2013_03_16-PM-06_55_01
Home
Index