Nuprl Definition : cauchy
cauchy(n.x[n]) == ∀k:ℕ+. (∃N:{ℕ| (∀n,m:ℕ. ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (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 :
cauchy
cauchy
Latex:
cauchy(n.x[n]) == \mforall{}k:\mBbbN{}\msupplus{}. (\mexists{}N:\{\mBbbN{}| (\mforall{}n,m:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} (N \mleq{} m) {}\mRightarrow{} (|x[n] - x[m]| \mleq{} (r1/r(k)))))\})
Date html generated:
2016_05_18-AM-07_38_09
Last ObjectModification:
2015_09_23-AM-09_02_18
Theory : reals
Home
Index