Theorem totallySeparatedSpace_of_t0_of_basis_clopen

Modification history

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