Lindelöf and paracompact spaces

[grunweg]

Inspired by PR #7160. Here are some possible steps, non-exhaustive :-)

Lindelöf spaces

• [x] definition (every open cover has a countable subcover)
• [x] #9168
• [x] $\sigma$-compact spaces are Lindelöf
• [x] basic properties: countable unions, images of Lindelöf sets and spaces are Lindelöf
• [ ] follow-up: adapt e.g. CompactExhaustion.choice to ask for Lindelöf instead; audit comments mentioning "Lindelöf"

extension: hereditarily Lindelöf spaces

• [x] definition: every subspace is Lindelöf (see pi-base)
• [x] Lindelöf implies hereditarily Lindelöf
• [ ] a Lindelöf $G_\delta$ space is hereditarily Lindelöf
• [x] secound countable implies hereditarily Lindelöf

Paracompact spaces

• [x] definition
• [x] locally compact and sigma-compact spaces are paracompact, in particular compact spaces are paracompact
• [x] every metric space is paracompact

Corollary of both: a locally compact second countable Hausdorff space is paracompact.

Lots of potential for extensions, e.g.

• [x] locally compact + second countable implies $\sigma$-compact
• [ ] show these notions coincide over metric spaces

[ADedecker]

We have:

• ParacompactSpace
• paracompact_of_locallyCompact_sigmaCompact
• paracompact_of_compact
• EMetric.instParacompactSpace
• sigmaCompactSpace_of_locally_compact_second_countable

Could you update the issue to take this into account?

[grunweg]

Updated. Thanks for looking up which of these items already existed!

[grunweg]

9107 by @JADekker defines Lindelöf spaces, using filters.

[JADekker]

9107 (or a follow-up PR) is scheduled to have a theorem that relates the filter definition to the countable subcover definition, I'll tick the first item when that is the case. If I get sufficiently close to the results in 2 - 5, I might include some of them at some point. I'm not yet sure about whether I'll work on anything with hereditarily Lindelöf spaces.

[JADekker]

9107 is awaiting review and has:

• definition of Lindelöf spaces in terms of filters
• some basic API for Lindelöf spaces
• theorems that show that this definition is equivalent to the usual one in terms of countable subcovers

Proving second countable spaces are Lindelöf should be relatively easy to add after this PR has passed.

[JADekker]

1., 2. and 4. are now in #9107 and/or scheduled in follow-up PR's. 3. should be relatively easy to add once #9107 and some follow-up PR's that I'll make have merged. Definition of Hereditarily Lindelöf + Second countable implies H. Lindelöf are also in #9107. Perfect normal + Hereditarily Lindelöf should be accessible now. I'm not sure about G_delta spaces, I haven't checked whether the API I wrote would easily accommodate for these, but I would expect it to be relatively straightforward. I'd have to take a good look to see how/if CompactExhaustion.choice would extend.

[JADekker]

9107 is merged now, I've updated the list accordingly.