Nuprl Definition : is-msfun

is-msfun(X;d;Y;d';f) ==  ∀x1,x2:X.  (f[x1] # f[x2] ⇒ x1 # x2)


Definitions occuring in Statement :  msep: x # y,  so_apply: x[s],  all: ∀x:A. B[x],  implies: P ⇒ Q
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q,  so_apply: x[s],  msep: x # y
FDL editor aliases :  is-msfun
Latex:
is-msfun(X;d;Y;d';f)  ==    \mforall{}x1,x2:X.    (f[x1]  \#  f[x2]  {}\mRightarrow{}  x1  \#  x2)


Date html generated: 2019_10_30-AM-06_25_12
Last ObjectModification: 2019_10_02-AM-10_00_40

Theory : reals


Home Index