Cocountable filter

Stream: mathlib4

[Josha Dekker]

Is there code for the filter generated by cocountable sets, e.g. similar to Order/Filter/Cofinite? I could add some more results to Topology/Compactness/Lindelof (see #9107, I have some follow-up PR's ready) if this was implemented; so I'm happy to add it if necessary!

[Yaël Dillies]

Try in stream #Is there code for X? !

[Yaël Dillies]

But also the answer is no

[Josha Dekker]

Sorry, wrong channel. Do you think it is okay if I write a small section on this similar to Order/Filter/Cofinite?

[Yaël Dillies]

Maybe! Is it meaningful mathematically?

[Josha Dekker]

It would be a good tool to conclude e.g. that countable discrete spaces are Lindelöf spaces, in a similar way to how cofinite filters are used to show that finite discrete spaces are compact

[Yaël Dillies]

Then sure go for it!

[Yury G. Kudryashov]

Another application of the cocountable filter: prove NeBot (nhds x ⊓ cocountable) (e.g., if x is a non-isolated point in a complete metric space), a.k.a. ∀ s ∈ nhds x, Uncountable s.

[Josha Dekker]

Yury G. Kudryashov said:

Another application of the cocountable filter: prove NeBot (nhds x ⊓ cocountable) (e.g., if x is a non-isolated point in a complete metric space), a.k.a. ∀ s ∈ nhds x, Uncountable s.

That’s a good one to add, do you know if it is already in mathlib somewhere? Otherwise I’m happy to try and add it at some point! I’ll probably make a PR for Filter.Cocountable after Christmas, or I could try to squeeze in a smaller one today; I have formalized some 10-20 results I guess…

[Yury G. Kudryashov]

You can open a PR with existing lemmas, then we'll either merge it and add more later, or add lemmas to it before merging. Anyway, it will be visible already.

[Josha Dekker]

I’ll wait with the cocountable one until the Uncountable one has merged, because some fundamental components would have to be refactored. I’ll try and squeeze in the PR for Uncountable somewhere the coming days!

[Josha Dekker]

I’d have to replace my usage of \not Countable by Uncountable everywhere, better to not have an intermediate version floating around