Nuprl Definition : real-fun

real-fun(f;a;b) ==  ∀x,y:{x:ℝx ∈ [a, b]} .  ((x y)  ((f x) (f y)))



Definitions occuring in Statement :  rccint: [l, u] i-member: r ∈ I req: y real: all: x:A. B[x] implies:  Q set: {x:A| B[x]}  apply: a
Definitions occuring in definition :  apply: a req: y implies:  Q rccint: [l, u] i-member: r ∈ I real: set: {x:A| B[x]}  all: x:A. B[x]
FDL editor aliases :  real-fun

Latex:
real-fun(f;a;b)  ==    \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))



Date html generated: 2016_07_08-PM-06_02_23
Last ObjectModification: 2016_07_05-PM-02_41_18

Theory : reals


Home Index