Nuprl Definition : fun-converges-to

Like our definition of continuouswe quantify only over ∈ of the form (r1/r(k))
  and compact subintervals of the form i-approx(I;m).⋅

lim n→∞.f[n; x] = λy.g[y] for x ∈ ==
  ∀m:{m:ℕ+icompact(i-approx(I;m))} . ∀k:ℕ+.
    ∃N:ℕ+. ∀x:{x:ℝx ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n; x] g[x]| ≤ (r1/r(k)))

Definitions occuring in Statement :  icompact: icompact(I) i-approx: i-approx(I;n) i-member: r ∈ I rdiv: (x/y) rleq: x ≤ y rabs: |x| rsub: y int-to-real: r(n) real: int_upper: {i...} nat_plus: + all: x:A. B[x] exists: x:A. B[x] set: {x:A| B[x]}  natural_number: $n
Definitions occuring in definition :  icompact: icompact(I) exists: x:A. B[x] nat_plus: + set: {x:A| B[x]}  real: i-member: r ∈ I i-approx: i-approx(I;n) all: x:A. B[x] int_upper: {i...} rleq: x ≤ y rabs: |x| rsub: y rdiv: (x/y) natural_number: $n int-to-real: r(n)
FDL editor aliases :  fun-converges-to

lim  n\mrightarrow{}\minfty{}.f[n;  x]  =  \mlambda{}y.g[y]  for  x  \mmember{}  I  ==
    \mforall{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  .  \mforall{}k:\mBbbN{}\msupplus{}.
        \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .  \mforall{}n:\{N...\}.    (|f[n;  x]  -  g[x]|  \mleq{}  (r1/r(k)))

Date html generated: 2016_11_09-AM-06_22_05
Last ObjectModification: 2016_11_08-AM-10_59_11

Theory : reals

Home Index