Hausdorff–Alexandroff theorem

Stream: PR reviews

[Vasilii Nesterov]

I've proved the Hausdorff–Alexandroff theorem: every compact metric space is a continuous image of the Cantor set.

[Vasilii Nesterov]

#26001: some auxiliary lemmas about the Cantor set

[Vasilii Nesterov]

Then I needed to prove that the Cantor set consists of numbers whose base-3 representations do not contain any 1s. To do that, I developed some API for representing real numbers in positional notation:

[Vasilii Nesterov]

#26004: auxiliary lemma about Nat.floor

[Vasilii Nesterov]

#26021: reals in positional notation

[Vasilii Nesterov]

#26096: the Cantor set is the set of 0-2 ternary numbers

[Vasilii Nesterov]

#26136: the Cantor set is homeomorphic to ℕ → Bool

[Vasilii Nesterov]

#26027: any compact metric space is homeomorphic to some closed subset of the Hilbert cube (ℕ → unitInterval)

[Vasilii Nesterov]

#26149: there is a continuous surjection from the Cantor space (ℕ → Bool) to the Hilbert cube.

[Vasilii Nesterov]

#26184: any closed subset of the Cantor space is a continous image of the Cantor space & Hausdorff–Alexandroff theorem

[Vasilii Nesterov]

As a simple corollary, I proved the existence of the Peano curve - a continuous surjection from the unit interval onto the unit square: #26185