Theorem totallyDisconnectedSpace_iff_connectedComponent_one

Modification history

2026-02-17 15:21
Mathlib/Topology/Algebra/Group/Basic.lean
feat(Topology/Algebra/Group/Basic): group is totally disconnected iff `connectedComponent 1 = {1}` (#35404) …
Added totallyDisconnectedSpace_iff_connectedComponent_oneView on Github →