Nuprl Definition : mtb-cantor-map

Given a point p in mtb-cantor(mtb), the sequence mtb-seq(mtb;p) may not
be Cauchy, but its regularization m-regularize(d;mtb-seq(mtb;p)) is
(and λk.(6 * k) is a witness -- modulus of Cauchyness -- for that).
Thus (given a witness cmplt for the completenss of X) it converges
to a point in X.

So we get a map from the general Cantor space, mtb-cantor(mtb), to X.
It is onto X  (Error :mtb-cantor-map-onto) and is uniformly
continuous (Error :mtb-cantor-map-continuous).
Hence, every compact metric space is the continuous image of a Cantor
space.

We get an even stronger version Error :mtb-cantor-map-onto-common
of the onto property of this map. It says that for points x and y in X
that are withing 1/(n+1) of each other (mdist(d;x;y) ≤ (r1/r(n + 1)))
then we can find points p and q in mtb-cantor(mtb) such that
p maps to x (mtb-cantor-map(d;cmplt;mtb;p) ≡ x) and q maps to y
(mtb-cantor-map(d;cmplt;mtb;q) ≡ y) and p and q agree on their first
n values  (they are equal in the type i:ℕn ⟶ ℕ(fst(mtb)) i).

Because of the theorem general-cantor-to-int-uniform-continuity,
 we can then prove that every FUNCTION
(f in X ⟶ ℝ for which ∀x,y:X.  (x ≡ y ⇒ ((f x) = (f y))) )
from a compact metric space to the reals is uniformly continuous.
(see Error :compact-metric-to-real-continuity).

Then, using the fact that ⌜X × X⌝ is also a compact metric space
(see m-TB-product and prod-metric-space-complete)
we can easily prove that every FUNCTION from X to a metric space Y
is uniformly continuous. Error :compact-metric-to-metric-continuity⋅
mtb-cantor-map(d;cmplt;mtb;p) ==  cauchy-mlimit(cmplt;m-regularize(d;mtb-seq(mtb;p));λk.(6 * k))


Definitions occuring in Statement :  m-regularize: m-regularize(d;s),  mtb-seq: mtb-seq(mtb;s),  cauchy-mlimit: cauchy-mlimit(cmplt;x;c),  lambda: λx.A[x],  multiply: n * m,  natural_number: $n
Definitions occuring in definition :  cauchy-mlimit: cauchy-mlimit(cmplt;x;c),  m-regularize: m-regularize(d;s),  mtb-seq: mtb-seq(mtb;s),  lambda: λx.A[x],  multiply: n * m,  natural_number: $n
FDL editor aliases :  mtb-cantor-map
Latex:
mtb-cantor-map(d;cmplt;mtb;p)  ==    cauchy-mlimit(cmplt;m-regularize(d;mtb-seq(mtb;p));\mlambda{}k.(6  *  k))


Date html generated: 2019_10_30-AM-07_04_50
Last ObjectModification: 2019_10_11-PM-01_11_54

Theory : reals


Home Index