K-Lindelöf spaces ready

Stream: mathlib4

[Josha Dekker]

Hi, just wanted to mention that I've started working on K-Lindelöf spaces in #11800. As sanity check that my definition in terms of filters works, I've added all the API up to and including the theorem isKLindelof_iff_cardinal_subcover that establish that this is indeed the right definition. To keep the diff small, I think this is about the content I would like for this PR, I can flesh out the API in a follow-up. All feedback is welcome. This PR relies on some properties of CardinalInterFilter's that I'm adding in #11758, so I need that one to merge first. Feedback on that one is thus also very much welcome.

I'm also curious about your thoughts on the following:

• As most (but not all!) of the interest results require k to be a regular cardinal (IsRegular k) I could assume this from the offset at a slight loss of generality.
• I had some universe-issues, which is due to the fact that the cardinalities don't really seem to play together nicely. Whereas docs#Lindelöf sometimes has two different universes in a statement, I couldn't get that to work nicely, so I just worked with the cases where the universes agreed. I guess you can always lift to max u v if you want.

[Josha Dekker]

I'm not putting it on awaiting-review for now, as I don't want to waste too much reviewing time in case #11758 doesn't fully go through. Any feedback is still welcome though!

[Josha Dekker]

As #11758 has merged, I believe #11800 is now ready for review. Although it is a new file, it is a rather straightforward generalisation of Lindelöf spaces, which have already been added to Mathlib, so I believe that reviewing should be straightforward. If desired, I can also add prove the analogous 2/3 of the file and add it to this PR, but that might make matters a bit long. Let me know!