## Stream: maths

### Topic: paracompact spaces

#### Yury G. Kudryashov (Feb 24 2021 at 02:49):

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_spaceparacompact_space;
• [X] locally_compact_spacesigma_compact_spacet2_spaceparacompact_space;
• [X] emetric_spaceparacompact_space;
• [ ] paracompact_spacet2_spacenormal_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 (Feb 24 2021 at 02:49):

The PR will depend on #6328

#### Yury G. Kudryashov (Feb 24 2021 at 05:17):

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

#### Yury G. Kudryashov (Mar 02 2021 at 00:28):

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

Last updated: May 09 2021 at 10:11 UTC