Commit 2023-02-05 01:17 8971bb0f

View on Github →

feat: port Topology.Paracompact (#2036)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Paracompact.lean

added theorem normal_of_paracompact_t2

added theorem precise_refinement

added theorem precise_refinement_set

added theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis

added theorem refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set