Nuprl Definition : fun-cauchy
λn.f[n; x] is cauchy for x ∈ I ==
∀a:{a:ℕ+| icompact(i-approx(I;a))} . ∀k:ℕ+.
∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;a)} . ∀n,m:{N...}. (|f[n; x] - f[m; 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-cauchy
Latex:
\mlambda{}n.f[n; x] is cauchy for x \mmember{} I ==
\mforall{}a:\{a:\mBbbN{}\msupplus{}| icompact(i-approx(I;a))\} . \mforall{}k:\mBbbN{}\msupplus{}.
\mexists{}N:\mBbbN{}\msupplus{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;a)\} . \mforall{}n,m:\{N...\}. (|f[n; x] - f[m; x]| \mleq{} (r1/r(k)))
Date html generated:
2016_05_18-AM-09_52_59
Last ObjectModification:
2015_09_23-AM-09_14_01
Theory : reals
Home
Index