Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-06 11:31 0fa0d61e

View on Github →

feat(topology/paracompact): define paracompact spaces (#6395) Fixes #6391

Estimated changes

Modified docs/references.bib

Modified roadmap/topology/paracompact.lean

deleted theorem normal_of_paracompact_t2

deleted theorem paracompact_of_compact

deleted theorem paracompact_of_metric

deleted theorem paracompact_space.precise_refinement

added theorem roadmap.normal_of_paracompact_t2

added theorem roadmap.paracompact_of_compact

added theorem roadmap.paracompact_of_metric

added theorem roadmap.paracompact_space.precise_refinement

Modified src/data/real/ennreal.lean

added theorem ennreal.exists_inv_two_pow_lt

added theorem ennreal.inv_le_one

added theorem ennreal.one_le_inv

added theorem ennreal.pow_le_pow_of_le_one

Modified src/order/filter/bases.lean

Modified src/topology/basic.lean

added theorem closure_inter_open'

added theorem closure_nonempty_iff

deleted theorem is_closed_Union_of_locally_finite

added theorem locally_finite.closure

added theorem locally_finite.closure_Union

added theorem locally_finite.comp_injective

added theorem locally_finite.is_closed_Union

added theorem locally_finite.subset

deleted theorem locally_finite_subset

deleted theorem set.nonempty.closure

Modified src/topology/constructions.lean

Modified src/topology/metric_space/emetric_space.lean

added theorem uniformity_basis_edist_inv_two_pow

Created src/topology/paracompact.lean

added theorem normal_of_paracompact_t2

added theorem precise_refinement

added theorem precise_refinement_set

added theorem refinement_of_locally_compact_sigma_compact_of_nhds_basis

Modified src/topology/separation.lean

added theorem compact_exhaustion.is_closed

Modified src/topology/subset_properties.lean

added theorem is_compact.elim_nhds_subcover'

added theorem is_compact.elim_nhds_subcover