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
a:A fp-> B[a] == d:A List \mtimes{} (a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} B[a])
Date html generated:
2015_07_17-AM-09_15_22
Last ObjectModification:
2012_02_25-AM-11_05_16
Home
Index