Zulip Chat Archive

Stream: maths

Topic: paracompact spaces


view this post on Zulip 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)?

view this post on Zulip Yury G. Kudryashov (Feb 24 2021 at 02:49):

The PR will depend on #6328

view this post on Zulip Yury G. Kudryashov (Feb 24 2021 at 05:17):

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

view this post on Zulip 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