Lindelof spaces

Stream: Is there code for X?

[Yury G. Kudryashov]

I'm going to define these classes/predicates. Are there any preferences between the "countable subcover" definition and a filter-style definition like docs#is_compact but assuming docs#countable_Inter_filter?

[Yury G. Kudryashov]

I mean, which one should be the definition and which one should be an iff lemma?

[Yury G. Kudryashov]

(I don't care)

[Reid Barton]

If there's no other reason to prefer one definition over the other then I would generally prefer to make the definition be the usual textbook definition (in this case, the "countable subcover" one)

[Patrick Massot]

That would be inconsistent with the definition of compactness.

[Reid Barton]

Yeah, that doesn't bother me.

[Reid Barton]

I mean, for me this is a less important consideration than matching standard sources.

[Johan Commelin]

But if a definition in terms of filters means that it's easier to apply the substantive filter API, I think that's important. It's a fact of life that informal mathematics doesn't need to care about filters in topology/analysis. It's also a fact of life that they are a great tool in setting up a formal library in these subjects.

[Reid Barton]

I assume this is not relevant because Yury plans to have both formulations anyways, it is just a question of which one to label as the definition.

[Yaël Dillies]

Setting up the API is relevant to setting up the API. What do you mean?

[Yury G. Kudryashov]

The tfae lemma will be among the first 10 lemmas about is_lindelof anyway.

[Yury G. Kudryashov]

And it doesn't matter which line of tfae is called is_lindelof.

[Yury G. Kudryashov]

/me is away for 3.5 hours (teaching)

[Reid Barton]

What's special about the definition is that you can reach it by using jump-to-definition. We often say that one advantage of formalized mathematics is that you can find out what any term means by jumping to its definition. So it seems to me that the definition should be something easy to understand/align with your existing informal notion.

[Reid Barton]

Of course there can be considerations which are more important than this one, but when defining a Prop there generally aren't.

[Patrick Massot]

That's a good point.

[Bhavik Mehta]

On the other hand, perhaps the docstring can contain the informal notion and reference the lemma establishing equivalence while the definition itself can be less intuitively informally correct

[Kevin Buzzard]

Our definition of compact certainly doesn't coincide with what's in the books. IIRC I've lied in a docstring before -- maybe docs#module.projective ? I gave some hideous definition but just said in the docstring that it was the usual one

[Patrick Massot]

Come on Kevin, check your book.

[Patrick Massot]

This is TG I.9.1 Définition 1

[Patrick Massot]

Or maybe you mean we should write "quasi-compact".

[Reid Barton]

Bhavik Mehta said:

On the other hand, perhaps the docstring can contain the informal notion and reference the lemma establishing equivalence while the definition itself can be less intuitively informally correct

If there's some compelling reason to choose a definition other than the "standard" one (e.g., if there are multiple equally standard informal definitions) then we should certainly have a docstring reference to lemmas that reinterpret the definition.

[Yury G. Kudryashov]

I already wrote tfae based on the open subcover definition, and I don't want to rewrite it.

[Yury G. Kudryashov]

(it's not that difficult, just I'm lazy)

[Yury G. Kudryashov]

How should I name the following lemma? Of course, I can use is_lindelof_of_strongly_lindelof_space but I would prefer to have something short.

lemma name_me {X : Type*} [topological_space X] [strongly_lindelof_space X] (s : set X) : is_lindelof s

[Kevin Buzzard]

Yury G. Kudryashov said:

(it's not that difficult, just I'm lazy)

Aren't you #1 on the list of PR people?? :-)

[Yury G. Kudryashov]

This doesn't mean that I want to rewrite the code without a good reason.

[Yury G. Kudryashov]

Also, I have a sore throat and 2 kids at home. This reduces my productivity.

[Yaël Dillies]

Get them to learn Lean. There's no problem, only solutions :rofl:

[Yury G. Kudryashov]

There is a dependency: to learn Lean, you need to learn the alphabet first. The dependency is not yet satisfied for one of them.

[Yury G. Kudryashov]

With Lindelöf spaces, we have the following possible instance loop:

• sigma_compact_space X → lindelof_space X;
• lindelof_space X → locally_compact_space X → sigma_compact_space X.

Currently, the latter instance assumes second_countable_topology X, thus does not create a loop. Which of the two lemmas should be an instance?

[Johan Commelin]

Any reason to believe that either of the two will be used less than the other?

[Patrick Massot]

I would guess sigma compact is more common. I hear of Lindelöf spaces very late, and I don't think I ever used that word before this sentence.

[Yury G. Kudryashov]

Of course, σ-compact is more common. The question is which instance will be more useful. I suggest that we have instances for sigma_compact_space X → lindelof_space X and second_countable_topology X → locally_compact_space X → sigma_compact_space X. The latter instance is a 1-liner on top of a non-instance lemma lindelof_space X → locally_compact_space X → sigma_compact_space X.