Nuprl Definition : is-mfun

f:FUN(X;Y) ==  ∀x1,x2:X.  (x1 ≡ x2 ⇒ f[x1] ≡ f[x2])


Definitions occuring in Statement :  meq: 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,  meq: x ≡ y,  so_apply: x[s]
FDL editor aliases :  is-mfun is-mfun
Latex:
f:FUN(X;Y)  ==    \mforall{}x1,x2:X.    (x1  \mequiv{}  x2  {}\mRightarrow{}  f[x1]  \mequiv{}  f[x2])


Date html generated: 2019_10_29-AM-11_15_18
Last ObjectModification: 2019_10_02-AM-09_55_39

Theory : reals


Home Index