Working on Lindelöf spaces

Stream: mathlib4

[Josha Dekker]

I've started formalising Lindelöf spaces and their basic API analogously to Compact spaces, let me know if you'd like an up-to-date version of what I have. (I have a PR out with the basic definitions, first theorems are in the making.)

[Yaël Dillies]

(PR is #9107)

[Josha Dekker]

Current progress is about the first 8-10 theorems defined as much verbatim as possible from Compact (I’m still filling in one gap). I’ll make a PR with them soon, to keep the number of lines low (around 150).

[Josha Dekker]

PR #9107 now updated.

[Josha Dekker]

PR #9107 now updated, it now establishes equivalence between the filter-based definition and the countable subcover definition.

[Josha Dekker]

I have completed most of the API for Lindelöf spaces now; I will start making PR's to add the various components once #9107 has been reviewed, to keep the amount to review manageable. I'm not sure how long that will take.

Some important omissions are related to the fact that I'm not sure how to rephrase the Lindelöf property in terms of ultrafilters; this would make the majority of the omissions feasible/accessible. I could try to work directly from the property, but that feels very inefficient.

Also missing are some analogues for cocompact <-> cofinite, this would require a cocountable filter, of which I'm not sure if it has been implemented?

[Josha Dekker]

I think most of the basic Lindelöf space things are in #9107 now, @Yury G. Kudryashov what do you think?

[Yury G. Kudryashov]

I'll have a look tomorrow, right after the "complex log" PR.

[Josha Dekker]

Thank you!