mathlib

c476f200 - feat(topology/algebra/group): discrete subgroup acts properly discontinuously (#16593)

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. Co-authored-by: Alex Kontorovich <58564076+AlexKontorovich@users.noreply.github.com>