### Nuprl Definition : fun-converges-to

`Like our definition of continuous, we 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 ∈ I ==`
`  ∀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: `x - 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: `x - y` rdiv: `(x/y)` natural_number: `\$n` int-to-real: `r(n)`
FDL editor aliases :  fun-converges-to

Latex:
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