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