Nuprl Definition : atom-free-decl

AtomFree(d) ==  ∀x∈dom(d). A=d(x) ⇒  atom-free{1:n}(Type; A)


Definitions occuring in Statement :  fpf-all: ∀x∈dom(f). v=f(x) ⇒  P[x; v],  universe: Type
Definitions occuring in definition :  fpf-all: ∀x∈dom(f). v=f(x) ⇒  P[x; v],  universe: Type
FDL editor aliases :  atom-free-decl
Latex:
AtomFree(d)  ==    \mforall{}x\mmember{}dom(d).  A=d(x)  {}\mRightarrow{}    atom-free\{1:n\}(Type;  A)


Date html generated: 2018_05_21-PM-09_30_30
Last ObjectModification: 2018_02_09-AM-10_25_03

Theory : finite!partial!functions


Home Index