Nuprl Definition : mtb-seq

When mtb is a witness that metric space X is totally bounded
and s is a point in the general Cantor space, mtb-cantor(mtb),
then at each natural number k there are finitely many points xs(k)
(that every other point in X is within 1/(k+1) of one of them),
and s(k) is the index of one of these points.

Thus we get a sequence of points in X.
Not every such sequence will converge in X, but for every point p
in X there is always one, coming from mtb-point-cantor(mtb;p),
that does converge to p (see Error :mtb-seq-mtb-point-cantor-mconverges-to).
⋅

mtb-seq(mtb;s) == let B,xs,c = mtb in λk.(xs k (s k))

Definitions occuring in Statement : spreadn: spread3, apply: f a, lambda: λx.A[x]
Definitions occuring in definition : spreadn: spread3, lambda: λx.A[x], apply: f a
FDL editor aliases : mtb-seq

Latex:
mtb-seq(mtb;s) == let B,xs,c = mtb in \mlambda{}k.(xs k (s k)) Date html generated: 2019_10_30-AM-06_56_06 Last ObjectModification: 2019_10_11-PM-00_28_13 Theory : reals Home Index