Nuprl Definition : continuous

Bishop defines f[x] to be continuous on compact interval if
for every ∈ > there is delta > 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 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 ∈ > 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 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 ∈ ==
  ∀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: y int-to-real: r(n) real: nat_plus: + all: x:A. B[x] sq_exists: x:{A| B[x]} implies:  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:  Q rleq: x ≤ y rabs: |x| rsub: y rdiv: (x/y) natural_number: $n int-to-real: r(n)
FDL editor aliases :  continuous

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