Nuprl Definition : es-interface-filter
X|a.P[a] == λb.if (#(b) =z 1) then [a∈b|P[a]] else {} fi o X
Definitions occuring in Statement :
eclass-compose1: f o X,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
lambda: λx.A[x],
natural_number: $n,
bag-size: #(bs),
bag-filter: [x∈b|p[x]],
empty-bag: {}
FDL editor aliases :
es-interface-filter
Latex:
X|a.P[a] == \mlambda{}b.if (\#(b) =\msubz{} 1) then [a\mmember{}b|P[a]] else \{\} fi o X
Date html generated:
2016_05_16-PM-10_51_00
Last ObjectModification:
2012_02_25-PM-01_49_18
Theory : event-ordering
Home
Index