[Merged by Bors] - feat: Add Uncountable

[JADekker]

Adds the Uncountable class to Countable/Defs and some basic API.

---

More to follow, but I'd like to get feedback on the way of writing first!

[alexjbest]

Do you have a link to the other things you want to add?

[JADekker]

Thanks, I’ll take a look at any remaining adjustments soon, but I see that @urkud is only working busily on this, thank you!

@alexjbest, let me start by providing some short background:

the reason why I’m implementing this is that I’m working on Lindelöf spaces in #9107. I’d like to introduce the cocountable filter (analogous to the way the cofinite filter is used for Compact spaces) and it came up in discussions on Zulip that, rather than writing \neg Countable at some points in the definitions, it might be nicer to have Uncountable.

As such I’ll mirror the contents from Countable/Basic for Uncountable, but after that I’ll probably only add whatever comes up that I need to define cocountable filters (but I’ll try to prove and add sufficiently general versions of whatever I’m using).

[urkud]

I'm done working on this branch. I think that this PR needs the instance for functions I posted on Zulip and the docstring fix suggested by Alex; otherwise it's ready. The instance should probably go to Data/Fintype/Card, because you'll need Infinite.natEmbedding.

[JADekker]

Great, will try to do this in a few days; if anyone has time and wants to add them, feel free of course! I’ll send a heads-up when I continue working on this.

[JADekker]

@urkud Do you mean the instance
[Uncountable α] : NeBot (cocountable α)
that you suggested in Zulip, or do you mean another one? This one requires the definition of the cocountable filter which I haven't PR'ed yet, and requires filters, so I think Data/Fintype/Card may be too far upstream (as I'll need to get NeBot, which comes from Filter/Basic). Perhaps I should include it in the PR for Filter/Cocountable when this PR gets merged? I suggest that I make a new PR that defines the cocountable filter once this PR and #9200 have merged; I can add this instance to that!

[urkud]

Thanks! 🎉
bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style