Nuprl Definition : proper-continuous
f[x] (proper)continuous for x ∈ I ==
∀m:{m:ℕ+| icompact(i-approx(I;m)) ∧ iproper(i-approx(I;m))} . ∀n:ℕ+.
(∃d:{ℝ| ((r0 < d)
∧ (∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n))))))})
Definitions occuring in Statement :
icompact: icompact(I),
i-approx: i-approx(I;n),
i-member: r ∈ I,
iproper: iproper(I),
rdiv: (x/y),
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
nat_plus: ℕ+,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
int-to-real: r(n),
natural_number: $n,
rdiv: (x/y),
rsub: x - y,
rabs: |x|,
rleq: x ≤ y,
implies: P ⇒ Q,
i-approx: i-approx(I;n),
i-member: r ∈ I,
real: ℝ,
all: ∀x:A. B[x],
rless: x < y,
and: P ∧ Q,
sq_exists: ∃x:{A| B[x]},
nat_plus: ℕ+,
iproper: iproper(I),
icompact: icompact(I),
set: {x:A| B[x]}
FDL editor aliases :
proper-continuous
Latex:
f[x] (proper)continuous for x \mmember{} I ==
\mforall{}m:\{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m)) \mwedge{} iproper(i-approx(I;m))\} . \mforall{}n:\mBbbN{}\msupplus{}.
(\mexists{}d:\{\mBbbR{}| ((r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;m))
{}\mRightarrow{} (y \mmember{} i-approx(I;m))
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r(n))))))\})
Date html generated:
2016_10_26-AM-09_43_07
Last ObjectModification:
2016_09_05-AM-10_01_43
Theory : reals
Home
Index