Nuprl Definition : mtb-cantor

When mtb is witness to metric space X being totally bounded,
the first component of mtb is a function B of type ⌜ℕ ⟶ ℕ⁺⌝.
This gives us a "general Cantor space" k:ℕ ⟶ ℕB[k]⋅

mtb-cantor(mtb) == k:ℕ ⟶ ℕ(fst(mtb)) k

Definitions occuring in Statement : int_seg: {i..j^-}, nat: ℕ, pi1: fst(t), apply: f a, function: x:A ⟶ B[x], natural_number: $n
Definitions occuring in definition : function: x:A ⟶ B[x], nat: ℕ, int_seg: {i..j^-}, natural_number: $n, apply: f a, pi1: fst(t)
FDL editor aliases : mtb-cantor

Latex:
mtb-cantor(mtb) == k:\mBbbN{} {}\mrightarrow{} \mBbbN{}(fst(mtb)) k Date html generated: 2019_10_30-AM-06_55_25 Last ObjectModification: 2019_10_11-PM-00_24_52 Theory : reals Home Index