Theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set

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_basis_setView on Github →
2023-02-05 01:17
Mathlib/Topology/Paracompact.lean
feat: port Topology.Paracompact (#2036)
Added refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_setView on Github →