# Zulip Chat Archive

## 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_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 (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