Commit 2021-07-23 08:09 970b17bf

refactor(topology/metric_space): move lemmas about paracompact_space and the shrinking lemma to separate files (#8404) Only a few files in mathlib actually depend on results about paracompact_space. With this refactor, only a few files depend on topology/paracompact_space and topology/shrinking_lemma. The main side effects are that paracompact_of_emetric and normal_of_emetric instances are not available without importing topology.metric_space.emetric_paracompact and the shrinking lemma for balls in a proper metric space is not available without import topology.metric_space.shrinking_lemma.