Nuprl Definition : mconverges-to
lim n→∞.x[n] = y == ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (mdist(d;x[n];y) ≤ (r1/r(k)))))])
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rdiv: (x/y),
rleq: 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,
mdist: mdist(d;x;y),
rdiv: (x/y),
natural_number: $n,
int-to-real: r(n)
FDL editor aliases :
mconverges-to
Latex:
lim n\mrightarrow{}\minfty{}.x[n] = y == \mforall{}k:\mBbbN{}\msupplus{}. (\mexists{}N:\mBbbN{} [(\mforall{}n:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} (mdist(d;x[n];y) \mleq{} (r1/r(k)))))])
Date html generated:
2019_10_30-AM-06_37_46
Last ObjectModification:
2019_10_02-AM-10_50_49
Theory : reals
Home
Index