paracompact spaces

Stream: maths

[Yury G. Kudryashov]

Hi, I've formalized a few facts about paracompact spaces in branch#paracompact, thanks a lot @Reid Barton for writing a roadmap with useful links. I'm going to fix docs and PR it tonight. I'm going to add the following lemmas/instances (checkmarks show already formalized lemmas):

• [X] compact_space → paracompact_space;
• [X] locally_compact_space → sigma_compact_space → t2_space → paracompact_space;
• [X] emetric_space → paracompact_space;
• [ ] paracompact_space → t2_space → normal_space.

Which of them should be instances? Should I add more instances/lemmas (besides partition of unity which is planned for the next PR)?

[Yury G. Kudryashov]

The PR will depend on #6328

[Yury G. Kudryashov]

@Patrick Massot @Sebastien Gouezel @Heather Macbeth :up:

[Yury G. Kudryashov]

For "metric spaces are paracompact" I formalized the proof by Mary Ellen Rudin. She constructs the sets of the refinement as some infinite unions of balls. In some cases (e.g., for a proper metric space) it is possible to find a locally finite refinement such that all sets are open balls. Is it true in the general case? @Patrick Massot @Sebastien Gouezel