Nuprl Definition : mdiverges
n.x[n]↑ == ∃e:ℝ. ((r0 < e) ∧ (∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ mdist(d;x[m];x[n])))))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rleq: x ≤ y,
rless: x < y,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
real: ℝ,
rless: x < y,
int-to-real: r(n),
natural_number: $n,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
nat: ℕ,
and: P ∧ Q,
le: A ≤ B,
rleq: x ≤ y,
mdist: mdist(d;x;y)
FDL editor aliases :
mdiverges
Latex:
n.x[n]\muparrow{} == \mexists{}e:\mBbbR{}. ((r0 < e) \mwedge{} (\mforall{}k:\mBbbN{}. \mexists{}m,n:\mBbbN{}. ((k \mleq{} m) \mwedge{} (k \mleq{} n) \mwedge{} (e \mleq{} mdist(d;x[m];x[n])))))
Date html generated:
2019_10_30-AM-06_41_09
Last ObjectModification:
2019_10_02-AM-10_53_52
Theory : reals
Home
Index