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
Latex:
fpf-restrict(f;P)  ==    mk\_fpf(filter(P;fpf-domain(f));snd(f))


Date html generated: 2016_05_16-AM-11_33_03
Last ObjectModification: 2012_02_25-AM-11_13_22

Theory : event-ordering


Home Index