Nuprl Definition : fpf-join
f ⊕ g == <(fst(f)) @ filter(λa.(¬ba ∈ dom(f));fst(g)), λa.f(a)?g(a)>
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,
bnot: ¬bb,
pi1: fst(t),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
append: as @ bs,
filter: filter(P;l),
bnot: ¬bb,
fpf-dom: x ∈ dom(f),
pi1: fst(t),
lambda: λx.A[x],
fpf-cap: f(x)?z,
fpf-ap: f(x)
FDL editor aliases :
fpf-join
Latex:
f \moplus{} g == <(fst(f)) @ filter(\mlambda{}a.(\mneg{}\msubb{}a \mmember{} dom(f));fst(g)), \mlambda{}a.f(a)?g(a)>
Date html generated:
2018_05_21-PM-09_20_53
Last ObjectModification:
2018_02_09-AM-10_18_01
Theory : finite!partial!functions
Home
Index