Nuprl Definition : diverges
n.x[n]↑ == ∃e:ℝ. ((r0 < e) ∧ (∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |x[m] - x[n]|))))
Definitions occuring in Statement :
rleq: x ≤ y,
rless: x < y,
rabs: |x|,
rsub: 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,
rabs: |x|,
rsub: x - y
FDL editor aliases :
diverges
diverges
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{} |x[m] - x[n]|))))
Date html generated:
2016_05_18-AM-07_36_06
Last ObjectModification:
2015_09_23-AM-09_02_06
Theory : reals
Home
Index