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.