Commit 2022-10-10 16:26 c476f200
View on Github →feat(topology/algebra/group): discrete subgroup acts properly discontinuously (#16593) A discrete subgroup of a topological group acts properly discontinuously on the left and on the right. Here discrete means finite intersection with any compact subset.