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
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
band: p ∧b q,
fpf-dom: x ∈ dom(f),
append: as @ bs,
filter: filter(P;l),
apply: f a,
fpf-ap: f(x),
fpf-cap: f(x)?z,
nil: []
FDL editor aliases :
fpf-union
Latex:
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:
2018_05_21-PM-09_18_08
Last ObjectModification:
2018_02_09-AM-10_16_59
Theory : finite!partial!functions
Home
Index