Nuprl Definition : fpf-union

fpf-union(f;g;eq;R;x) ==  if x ∈ dom(f) ∧b x ∈ dom(g) then f(x) @ filter(R f(x);g(x)) else f(x)?g(x)?[] fi 



Definitions occuring in Statement :  fpf-cap: f(x)?z,  fpf-ap: f(x),  fpf-dom: x ∈ dom(f),  filter: filter(P;l),  append: as @ bs,  nil: [],  band: p ∧b q,  ifthenelse: if b then t else f fi ,  apply: f a
FDL editor aliases :  fpf-union
fpf-union(f;g;eq;R;x)  ==
    if  x  \mmember{}  dom(f)  \mwedge{}\msubb{}  x  \mmember{}  dom(g)  then  f(x)  @  filter(R  f(x);g(x))  else  f(x)?g(x)?[]  fi 



Date html generated: 2015_07_17-AM-09_16_38
Last ObjectModification: 2012_02_25-AM-11_06_26

Home Index