Nuprl Definition : mtb-point-cantor
For a point p in X, this gives the sequence of indexes to the points
that are better and better "approximations" to p.
So, it is a point s in the general Cantor space mtb-cantor(mtb)
and mtb-seq(mtb;s) is a Cauchy sequence (in fact, a regular sequence) that
converges to p.⋅
mtb-point-cantor(mtb;p) == let B,xs,c = mtb in c p
Definitions occuring in Statement :
spreadn: spread3,
apply: f a
Definitions occuring in definition :
spreadn: spread3,
apply: f a
FDL editor aliases :
mtb-point-cantor
Latex:
mtb-point-cantor(mtb;p) == let B,xs,c = mtb in c p
Date html generated:
2019_10_30-AM-06_57_01
Last ObjectModification:
2019_10_11-PM-00_38_56
Theory : reals
Home
Index