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