Nuprl Definition : non-void-decl
non-void(d) ==  ∀x∈dom(d). A=d(x) 
⇒  A
Definitions occuring in Statement : 
fpf-all: ∀x∈dom(f). v=f(x) 
⇒  P[x; v]
Definitions occuring in definition : 
fpf-all: ∀x∈dom(f). v=f(x) 
⇒  P[x; v]
FDL editor aliases : 
non-void-decl
Latex:
non-void(d)  ==    \mforall{}x\mmember{}dom(d).  A=d(x)  {}\mRightarrow{}    A
Date html generated:
2018_05_21-PM-09_30_16
Last ObjectModification:
2018_02_09-AM-10_24_50
Theory : finite!partial!functions
Home
Index