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