Theorem CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum

Modification history

2025-09-12 10:33
Mathlib/Topology/Separation/Lemmas.lean
feat: countable metric spaces are totally disconnected (#29211) …
Added CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuumView on Github →