Nuprl Definition : fpf-restrict
fpf-restrict(f;P) ==  mk_fpf(filter(P;fpf-domain(f));snd(f))
Definitions occuring in Statement : 
mk_fpf: mk_fpf(L;f)
, 
fpf-domain: fpf-domain(f)
, 
filter: filter(P;l)
, 
pi2: snd(t)
FDL editor aliases : 
fpf-restrict
fpf-restrict(f;P)  ==    mk\_fpf(filter(P;fpf-domain(f));snd(f))
Date html generated:
2015_07_17-AM-11_14_35
Last ObjectModification:
2012_02_25-AM-11_13_22
Home
Index