any cover admits a countable subcover

Stream: Is there code for X?

[Yury G. Kudryashov]

Quite a few lemmas in measure theory depend on the following property of a set: any open cover of s admits a countable subcover. There are (at least) a few reasons for this to be true:

• the ambient space is a second countable topological space;
• the subtype is a second countable topological space;
• the set is compact;
• more generally, the set is σ-compact.

Currently, lemmas randomly choose between [second_countable_topology α] (e.g., docs#measure_theory.null_of_locally_null) and is_compact K (e.g., docs#measure_theory.is_mul_left_invariant.measure_pos_of_is_open) depending on the expected applications. Should we have a named predicate for this property? If yes, how should we call it?

[Reid Barton]

https://en.wikipedia.org/wiki/Lindel%C3%B6f_space?

[Yaël Dillies]

I think Yury wants a property of the set, not the type?

[Yaël Dillies]

This is really analogous to compacity, right? So what about countably_compact or quasicompact (which is apparently our compact when compact means compact + separated), or is_lindeloef?

[Reid Barton]

I think "countably compact" is usually used for the other way to add "countable": https://en.wikipedia.org/wiki/Countably_compact_space

[Yaël Dillies]

Oh, I see

[Yaël Dillies]

compact_countably, then? :upside_down:

[Yury G. Kudryashov]

I think that is_lindelof is better.

[Yury G. Kudryashov]

(and lindelof_space/strongly_lindelof_space for the space properties)