Nuprl Definition : converges-to
lim n→∞.x[n] = y == ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - y| ≤ (r1/r(k)))))})
Definitions occuring in Statement :
rdiv: (x/y),
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
int-to-real: r(n),
nat_plus: ℕ+,
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
implies: P ⇒ Q,
natural_number: $n
Definitions occuring in definition :
nat_plus: ℕ+,
sq_exists: ∃x:{A| B[x]},
all: ∀x:A. B[x],
nat: ℕ,
implies: P ⇒ Q,
le: A ≤ B,
rleq: x ≤ y,
rabs: |x|,
rsub: x - y,
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
converges-to
converges-to
Latex:
lim n\mrightarrow{}\minfty{}.x[n] = y == \mforall{}k:\mBbbN{}\msupplus{}. (\mexists{}N:\{\mBbbN{}| (\mforall{}n:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} (|x[n] - y| \mleq{} (r1/r(k)))))\})
Date html generated:
2016_05_18-AM-07_35_27
Last ObjectModification:
2015_09_23-AM-09_01_58
Theory : reals
Home
Index