Nuprl Definition : m-cont-real-fun
m-cont-real-fun(X;d;x.f[x]) ==
∀e:{e:ℝ| r0 < e} . ∃delta:{e:ℝ| r0 < e} . ∀x,x':X. ((mdist(d;x;x') < delta) ⇒ (|f[x] - f[x']| < e))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
int-to-real: r(n),
natural_number: $n,
all: ∀x:A. B[x],
implies: P ⇒ Q,
mdist: mdist(d;x;y),
rless: x < y,
rabs: |x|,
rsub: x - y
FDL editor aliases :
m-cont-real-fun
Latex:
m-cont-real-fun(X;d;x.f[x]) ==
\mforall{}e:\{e:\mBbbR{}| r0 < e\}
\mexists{}delta:\{e:\mBbbR{}| r0 < e\} . \mforall{}x,x':X. ((mdist(d;x;x') < delta) {}\mRightarrow{} (|f[x] - f[x']| < e))
Date html generated:
2019_10_30-AM-06_26_49
Last ObjectModification:
2019_10_02-AM-10_02_07
Theory : reals
Home
Index