Theorem CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum

Modification history

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