Nuprl Definition : mapfilter-class
(f[v] where v from X such that P[v]) ==  λv.if P[v] then {f[v]} else {} fi [X]
Definitions occuring in Statement : 
es-filter-image: f[X]
, 
ifthenelse: if b then t else f fi 
, 
lambda: λx.A[x]
, 
single-bag: {x}
, 
empty-bag: {}
FDL editor aliases : 
mapfilter-class
(f[v]  where  v  from  X  such  that  P[v])  ==    \mlambda{}v.if  P[v]  then  \{f[v]\}  else  \{\}  fi  [X]
Date html generated:
2015_07_17-PM-01_07_12
Last ObjectModification:
2012_02_25-PM-01_37_37
Home
Index