Talk:Lebesgue's Number Lemma/Sequentially Compact Space

This theorem can be proven for the more general case of compact metric spaces (by Sequentially Compact Metric Space is Compact). Should this page be moved to Lebesgue's Number Lemma for Sequentially Compact Spaces, or should I put that result in Lebesgue's Number Lemma for Compact Spaces? Personally, I'd favor the former.

On second thought, this should be hierarchical. So, this page should go to Lebesgue's Number Lemma/Sequentially Compact Space, and the general result put on the main page. --CircuitCraft (talk) 21:23, 11 October 2023 (UTC)

I think we could/should make a proof for the compact metric spaces version, and then add the sequentially compact version as a corollary.

But because for a metric space the proofs are of equivalent strength (a compact space is sequentially compact by definition, and a sequentially compact metric space is compact, so they are equivalent), it doesn't make much philosophical difference.

In short, it doesn't matter which way round they go, but it's good to follow the canon. So feel free to put a maintenance template in there of some kind, and we can get to it.

Anyone else care to weigh in here? --prime mover (talk) 23:32, 11 October 2023 (UTC)

Do we really need two pages for the same result? How about to weaken the assumption of this theorem to be compact, and add one line into proof about Sequentially Compact Metric Space is Compact. --Usagiop (talk) 23:18, 12 October 2023 (UTC)

Problem is, one of the proofs of Sequentially Compact Metric Space is Compact uses Lebesgue's Number Lemma on a sequentially compact space. That's why I want to preserve the current result as-is. --CircuitCraft (talk) 02:10, 13 October 2023 (UTC)

OK, sorry, then this should be a corollary. It is then also important that the general version will be equipped with another proof not depending on Sequentially Compact Metric Space is Compact --Usagiop (talk) 22:36, 13 October 2023 (UTC)

The reason we keep the result as-is is because it appears in that form in Sutherland. --prime mover (talk) 05:00, 13 October 2023 (UTC)

So we have this: compactness and sequential compactness are independent in a general topological space, but equivalent in a metric space. Hence you can start with sequential compactness and then argue this equivalence. So we have subpage for compact, subpage for sequentially compact, link together with an equivalence proof (or system of equivalence proofs, we take our time on this) and at the end the customer-facing "Lebesgue's Number Lemma" conceals all the heavy lifting by referring to the equivalence as necessary and passim.

Lovely work, this is all starting to shape up. --prime mover (talk) 06:40, 14 October 2023 (UTC)