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]
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:
2016_05_16-AM-11_02_35
Last ObjectModification:
2012_02_25-AM-11_05_16
Theory : event-ordering
Home
Index