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)
Definitions occuring in definition :
mk_fpf: mk_fpf(L;f),
filter: filter(P;l),
fpf-domain: fpf-domain(f),
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:
2018_05_21-PM-09_30_57
Last ObjectModification:
2018_02_09-AM-10_25_25
Theory : finite!partial!functions
Home
Index