Nuprl Definition : continuous
Bishop defines f[x] to be continuous on compact interval J if
for every ∈ > 0 there is a delta > 0 such that
∀x,y:ℝ. ((x ∈ J) ⇒ (y ∈ J) ⇒ (|x - y| ≤ delta) ⇒ (|f[x] - f[y]| ≤ ∈))
Bishop then defines f[x] to be continuous on an arbitrary interval I if
if it is continuous on every compact subinterval of I.
The constructive content of this definition is called the modulus of continuity
of f.
In order to keep the modulus of continuity simpler (but equivalent),
we modify this definition in two ways.
First, rather than quantify over all ∈ > 0 we can quantify over n > 0
and use (r1/r(n)) in place of ∈.
Second, rather than quantify over all compact subintervals of I, we
define a uniform family of compact subintervals i-approx(I;m), indexed by
m > 0, that "fill up" the interval I.
This modification give the modulus of continuity the type like
ℕ+ ⟶ ℕ+ ⟶ ℝ⋅
f[x] continuous for x ∈ I ==
∀m:{m:ℕ+| icompact(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,
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 :
set: {x:A| B[x]} ,
icompact: icompact(I),
nat_plus: ℕ+,
sq_exists: ∃x:{A| B[x]},
and: P ∧ Q,
rless: x < y,
all: ∀x:A. B[x],
real: ℝ,
i-member: r ∈ I,
i-approx: i-approx(I;n),
implies: P ⇒ Q,
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
continuous
Latex:
f[x] continuous for x \mmember{} I ==
\mforall{}m:\{m:\mBbbN{}\msupplus{}| icompact(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_11_08-AM-09_07_05
Last ObjectModification:
2016_11_07-PM-05_25_15
Theory : reals
Home
Index