Theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis

Modification history

2023-09-03 19:50
Mathlib/Topology/Paracompact.lean
feat: define weakly locally compact spaces (#6770)
Modified refinement_of_locallyCompact_sigmaCompact_of_nhds_basisView on Github →
2023-02-05 01:17
Mathlib/Topology/Paracompact.lean
feat: port Topology.Paracompact (#2036)
Added refinement_of_locallyCompact_sigmaCompact_of_nhds_basisView on Github →