Nuprl Definition : real-sfun
real-sfun(f;a;b) == ∀x,y:{x:ℝ| x ∈ [a, b]} . (f x ≠ f y ⇒ x ≠ y)
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
rneq: x ≠ y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
rneq: x ≠ y,
apply: f a,
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-sfun
Latex:
real-sfun(f;a;b) == \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (f x \mneq{} f y {}\mRightarrow{} x \mneq{} y)
Date html generated:
2016_07_08-PM-06_02_50
Last ObjectModification:
2016_07_05-PM-02_48_15
Theory : reals
Home
Index