Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_clopen_of_totally_separated

Modification history

2021-06-03 23:23
src/topology/connected.lean
feat(topology): A locally compact Hausdorff space is totally disconnected if and only if it is totally separated (#7649) …
Added exists_clopen_of_totally_separatedView on Github →