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: x = y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
apply: f a,
req: x = y,
implies: P ⇒ 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