Commit 2025-09-12 10:33 07c73630

View on Github →

feat: countable metric spaces are totally disconnected (#29211) Prove that countable metric spaces are totally disconnected. This can't be placed inside Mathlib.Topology.MetricSpace.Basic because it causes a circular import with Mathlib.Analysis.Real.Cardinality. See also Rat.instTotallyDisconnectedSpace. There is a reference here for the mathematical statement and proof. This is upstreamed from https://github.com/girving/ray.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Real/Cardinality.lean

added theorem Cardinal.Real.Icc_countable_iff

added theorem Cardinal.Real.Ico_countable_iff

added theorem Cardinal.Real.Ioc_countable_iff

added theorem Cardinal.Real.Ioo_countable_iff

Modified Mathlib/Topology/Separation/CompletelyRegular.lean

added theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum

Created Mathlib/Topology/Separation/Lemmas.lean

added theorem CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum

added theorem Set.Countable.isTotallyDisconnected

Modified Mathlib/Topology/Separation/Profinite.lean

added theorem totallySeparatedSpace_of_t0_of_basis_clopen

deleted theorem totallySeparatedSpace_of_t1_of_basis_clopen