Nuprl Definition : fin_spr
fin_spr(B) ==  {f:  | n:. ((f n)  (B mklist(n;f)))} 
Definitions occuring in Statement : 
nat: , 
le: A  B, 
all: x:A. B[x], 
set: {x:A| B[x]} , 
apply: f a, 
function: x:A  B[x], 
mklist: mklist(n;f)
FDL editor aliases : 
fin_spr
fin\_spr(B)  ==    \{f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}|  \mforall{}n:\mBbbN{}.  ((f  n)  \mleq{}  (B  mklist(n;f)))\} 
Date html generated:
2013_03_20-AM-10_34_24
Last ObjectModification:
2013_03_09-PM-06_27_53
Home
Index