mathlib

89928bc0 - feat(topology): A locally compact Hausdorff space is totally disconnected if and only if it is totally separated (#7649)

feat(topology): A locally compact Hausdorff space is totally disconnected if and only if it is totally separated (#7649) We prove that a locally compact Hausdorff space is totally disconnected if and only if it is totally separated.