Nuprl Definition : m-cont-metric-fun
m-cont-metric-fun(X;dX;Y;dY;x.f[x]) ==
∀e:{e:ℝ| r0 < e} . ∃delta:{e:ℝ| r0 < e} . ∀x,x':X. ((mdist(dX;x;x') < delta) ⇒ (mdist(dY;f[x];f[x']) < e))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rless: 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,
rless: x < y,
mdist: mdist(d;x;y)
FDL editor aliases :
m-cont-metric-fun
Latex:
m-cont-metric-fun(X;dX;Y;dY;x.f[x]) ==
\mforall{}e:\{e:\mBbbR{}| r0 < e\}
\mexists{}delta:\{e:\mBbbR{}| r0 < e\} . \mforall{}x,x':X. ((mdist(dX;x;x') < delta) {}\mRightarrow{} (mdist(dY;f[x];f[x']) < e))
Date html generated:
2019_10_30-AM-06_28_08
Last ObjectModification:
2019_10_02-AM-10_03_19
Theory : reals
Home
Index