Commit 2025-11-16 18:46 4682615d

feat(Topology): every compact metric space is image of Cantor set (#26184)

1. Add cantorToHilbert: a continuous surjection from the Cantor space (ℕ → Bool) to the Hilbert Cube (ℕ → unitInterval).
2. Prove exists_nat_bool_continuous_surjective_of_compact: for every nonempty compact metric space X there is a continuous surjection from the Cantor space to X. This is known as Hausdorff–Alexandroff theorem.
3. Add auxiliary constructions for homeomorphisms:

• Equiv.toHomeomorphOfDiscrete: any bijection between discrete spaces is a homeomorphism
• Homeomorph.piCurry: (X × Y → Z) ≃ₜ (X → Y → Z)