Nuprl Definition : fpf-is-empty
fpf-is-empty(f) == (||fst(f)|| =z 0)
Definitions occuring in Statement :
length: ||as||,
eq_int: (i =z j),
pi1: fst(t),
natural_number: $n
Definitions occuring in definition :
eq_int: (i =z j),
length: ||as||,
pi1: fst(t),
natural_number: $n
FDL editor aliases :
fpf-is-empty
Latex:
fpf-is-empty(f) == (||fst(f)|| =\msubz{} 0)
Date html generated:
2018_05_21-PM-09_17_39
Last ObjectModification:
2018_02_09-AM-10_16_40
Theory : finite!partial!functions
Home
Index