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