Nuprl Definition : fpf
a:A fp-> B[a] == d:A List × (a:{a:A| (a ∈ d)} ⟶ B[a])
Definitions occuring in Statement :
l_member: (x ∈ l),
list: T List,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
product: x:A × B[x]
Definitions occuring in definition :
product: x:A × B[x],
list: T List,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
l_member: (x ∈ l)
FDL editor aliases :
fpf
Latex:
a:A fp-> B[a] == d:A List \mtimes{} (a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} B[a])
Date html generated:
2018_05_21-PM-09_16_58
Last ObjectModification:
2018_02_09-AM-10_16_19
Theory : finite!partial!functions
Home
Index