Nuprl Definition : mcauchy
mcauchy(d;n.x[n]) == ∀k:ℕ+. (∃N:ℕ [(∀n,m:ℕ. ((N ≤ n) ⇒ (N ≤ m) ⇒ (mdist(d;x[n];x[m]) ≤ (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 :
mcauchy
Latex:
mcauchy(d;n.x[n]) ==
\mforall{}k:\mBbbN{}\msupplus{}. (\mexists{}N:\mBbbN{} [(\mforall{}n,m:\mBbbN{}. ((N \mleq{} n) {}\mRightarrow{} (N \mleq{} m) {}\mRightarrow{} (mdist(d;x[n];x[m]) \mleq{} (r1/r(k)))))])
Date html generated:
2019_10_30-AM-06_37_07
Last ObjectModification:
2019_10_02-AM-10_50_12
Theory : reals
Home
Index