Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.properly_discontinuous_smul_opposite_of_tendsto_cofinite

Modification history

2022-10-10 16:26
src/topology/algebra/group.lean
feat(topology/algebra/group): discrete subgroup acts properly discontinuously (#16593) …
Added subgroup.properly_discontinuous_smul_opposite_of_tendsto_cofiniteView on Github →