Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-03 23:23 89928bc0

View on Github →

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.

Estimated changes