Nuprl Definition : in_fin_spr
(f 
fspr(B)) == 
n:
. ((f n) 
(B mklist(n;f)))
Definitions occuring in Statement :
nat: ,
le: A B,
all: x:A. B[x],
apply: f a,
mklist: mklist(n;f)
FDL editor aliases :
in_fin_spr
(f \mmember{} fspr(B)) == \mforall{}n:\mBbbN{}. ((f n) \mleq{} (B mklist(n;f)))
Date html generated:
2013_03_20-AM-10_34_29
Last ObjectModification:
2013_03_16-PM-08_24_36
Home
Index