Theorem Subgroup.tendsto_coe_cofinite_of_isDiscrete

Modification history

2026-09-09 21:26
Mathlib/Topology/Algebra/OpenSubgroup.lean
feat: a locally closed subgroup is closed (#42501) …
Added Subgroup.tendsto_coe_cofinite_of_isDiscreteView on Github →