Hausdorff–Alexandroff Theorem

In this file, we prove the Hausdorff–Alexandroff theorem, which states that every nonempty compact metric space is a continuous image of the Cantor set.

Main theorems

• exists_nat_bool_continuous_surjective_of_compact: Hausdorff–Alexandroff Theorem.

Proof Outline

First, note that the Cantor set is homeomorphic to ℕ → Bool, as shown in cantorSetHomeomorphNatToBool. Therefore, in this file, we work only with the space ℕ → Bool and refer to it as the "Cantor space".

The proof consists of three steps. Let X be a compact metric space.

1. Every compact metric space is homeomorphic to a closed subset of the Hilbert cube. This is already proved in exists_closed_embedding_to_hilbert_cube. Using this result, we may assume that X is a closed subset of the Hilbert cube.
2. We construct a continuous surjection cantorToHilbert from the Cantor space to the Hilbert cube.
3. Taking the preimage of X under this surjection, it remains to prove that any closed subset of the Cantor space is the continuous image of the Cantor space.

noncomputable def Real.fromBinary : (ℕ → Bool) → ↑unitInterval

Convert a sequence of binary digits to a real number from unitInterval.

Equations

• Real.fromBinary = Subtype.coind (Real.ofDigits ∘ ⇑(Homeomorph.piCongrRight fun (x : ℕ) => finTwoEquiv.toHomeomorphOfDiscrete.symm)) Real.fromBinary._proof_2

theorem Real.fromBinary_continuous : Continuous fromBinary

theorem Real.fromBinary_surjective : Function.Surjective fromBinary

noncomputable def cantorToHilbert (x : ℕ → Bool) : ℕ → ↑unitInterval

A continuous surjection from the Cantor space to the Hilbert cube.

Equations

• cantorToHilbert x = Pi.map (fun (x : ℕ) (b : ℕ → Bool) => Real.fromBinary b) (cantorSpaceHomeomorphNatToCantorSpace x)

theorem cantorToHilbert_continuous : Continuous cantorToHilbert

theorem cantorToHilbert_surjective : Function.Surjective cantorToHilbert

theorem exists_retractionCantorSet {X : Set (ℕ → Bool)} (h_closed : IsClosed X) (h_nonempty : X.Nonempty) : ∃ (f : (ℕ → Bool) → ℕ → Bool), Continuous f ∧ Set.range f = X

theorem exists_nat_bool_continuous_surjective_of_compact (X : Type u_1) [Nonempty X] [MetricSpace X] [CompactSpace X] : ∃ (f : (ℕ → Bool) → X), Continuous f ∧ Function.Surjective f

Hausdorff–Alexandroff theorem: every nonempty compact metric space is a continuous image of the Cantor set.