Nuprl Definition : m-k-regular
This is the "metric" version of the notion of a (k)regular sequence
(that was used to define the real numbers).
Every (k)regular sequence is a Cauchy sequence (Error :m-k-regular-mcauchy)
so it will converge if the metric space X is complete.⋅
m-k-regular(d;k;s) == ∀n,m:ℕ. (mdist(d;s n;s m) ≤ ((r(k)/r(n + 1)) + (r(k)/r(m + 1))))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rdiv: (x/y),
rleq: x ≤ y,
radd: a + b,
int-to-real: r(n),
nat: ℕ,
all: ∀x:A. B[x],
apply: f a,
add: n + m,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
nat: ℕ,
rleq: x ≤ y,
mdist: mdist(d;x;y),
apply: f a,
radd: a + b,
rdiv: (x/y),
int-to-real: r(n),
add: n + m,
natural_number: $n
FDL editor aliases :
m-k-regular
Latex:
m-k-regular(d;k;s) == \mforall{}n,m:\mBbbN{}. (mdist(d;s n;s m) \mleq{} ((r(k)/r(n + 1)) + (r(k)/r(m + 1))))
Date html generated:
2019_10_30-AM-06_58_04
Last ObjectModification:
2019_10_11-PM-00_42_04
Theory : reals
Home
Index