Mathlib v3 is deprecated. Go to Mathlib v4

Theorem local_compact_nhds

Modification history

2022-01-25 17:30
src/topology/subset_properties.lean
feat(topology/algebra/mul_action2): quotient by a properly discontinuous group action is t2 (#10465) …
Added local_compact_nhdsView on Github →