Theorem IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty

Modification history

2025-12-22 22:40
Mathlib/Topology/Algebra/Group/Pointwise.lean
feat: covering maps from properly discontinuous actions and discrete subgroups (#7596)
Added IsDiscrete.exists_nhds_eq_one_of_image_mulLeft_inter_nonemptyView on Github →