Theorem exists_nat_bool_continuous_surjective_of_compact

Modification history

2025-11-16 18:46
Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean
feat(Topology): every compact metric space is image of Cantor set (#26184) …
Added exists_nat_bool_continuous_surjective_of_compactView on Github →