paracompact + locally compact + connected implies exhaustible by compacts

[Moniker1998]

See #1214

[prabau]

Reading your proof. I agree that the constructed $\bigcup_n L_n$ is an open set and is sigma-compact.

But it's not clear to me why it's also a closed set. Not sure actually what the next to last sentence in the big paragraph in the middle (starting with "If $y\in U_i$ and ...") is saying in this regard.

Added later:
I see now why $A=\bigcup_n L_n$ is closed. It's easy to see: if some element $y$ is not in$A$, and $y\in U_j$ for some $U_j\in\mathcal U$, then $U_j$ is necessarily disjoint from $A$ (easy to check, and what you intended to do with what you wrote).
I think that sentence in that paragraph should be changed to make things clear.

Also, another thing that would be helpful to explain why each $L_n$ is a finite union of compact sets: It's because any compact set can only meet finitely many members of a locally finite collection of sets (easy to check, no need for proof, but I think it would clarify the inductive construction of the $L_n$).

---

If you don't mind, it's the right thing to do to refer to this mathse answer for this pi-base result. But since this is going to be referenced in pi-base, it should be a little more self-contained. In the sense that one should not have to hunt down the details of the original question and of the other answers to make sense of what is being shown.
In particular, at the top of the answer it says "This holds even without ...". This is annoying, as one has no idea what "This" refers to, especially since different answers and comments at the top were showing different things not quite related to each other.

In other words, it would be helpful to clearly state at the top the result being shown in the answer, instead of making the reader guess what is going on and finally infer something at the end.

[yhx-12243]

In fact the condition of paracompact can be weaken to para-Lindelöf, see comment in that mathse post.

[Moniker1998]

@prabau @yhx-12243 I've addressed your issues Patrick, and by suggestion of yhx, I've replaced paracompact by para-Lindelöf, and since there is really nothing stopping me, I've changed locally compact to locally Lindelöf as well, which might some time arrive at pi-base.

---

Since clear definition of locally Lindelöf doesn't really exist in the literature from what I checked, maybe it's better not to add it though.

[prabau]

@Moniker1998 Thanks for the clear reorganization of the post. Very readable. (I fixed a minor thing in the post.)

About the main result (If X is locally Lindelöf and para-Lindelöf, then X is a union of pairwise disjoint clopen Lindelöf sets):

The proof shows that each $x\in X$ is in some clopen Lindelof set. But it still does not show that the whole space can be partitioned into these sets. I.e., starting with some $x$ one constructs $L=\bigcup_n L_n$ clopen Lindelof. Then one takes a $z\notin L$ and repeat the construction to get a clopen Lindelof set $M=\bigcup_n M_n$$ around $z$. But it could be that $M$ intersects $L$. Need to think more on this.

Corollary 1 is valid no matter what, but it would be good to prove the theorem also.

@yhx-12243 fyi

[prabau]

Regarding the notion of "locally Lindelöf", this should probably first be discussed in a separate issue, but I think it would be useful to add the definition in pi-base. And I am sure there are more results out there that make use of the notion, even if not by name.

But as for many "local properties", there are different variants, depending on whether one requires a local base of nbhds with the property around each point, or just one nbhd with the property around each point. Both notions are useful.
See https://github.com/pi-base/data/wiki/Conventions-and-Style#local-properties for the general convention used in pi-base to distinguish between the two.

In particular, we have

• Weakly locally compact (P23)
• Locally compact (P130)

(Each paper usually has to define what they mean exactly by "locally compact". But note that the term "weakly locally compact" is not just a pi-base invention. It does appear in a few cases in the literature (see references in https://en.wikipedia.org/wiki/Locally_compact_space, where it is also mentioned). At least it is clear and unambiguous. That convention makes it easy to distinguish between the two.

Similarly, there will be:

• Weakly locally Lindelöf
• Locally Lindelöf

For the mathse post, the notion is the first one.

In any case, I think it would be useful to edit the post to use this convention, i.e. rename "locally compact" to "weakly locally compact" and "locally Lindelöf" to "weakly locally Lindelöf" in your answer. That will keep things clear, and will match with what will be in pi-base eventually.

Opinions?

[Moniker1998]

@Moniker1998 Thanks for the clear reorganization of the post. Very readable. (I fixed a minor thing in the post.)

About the main result (If X is locally Lindelöf and para-Lindelöf, then X is a union of pairwise disjoint clopen Lindelöf sets):

The proof shows that each x ∈ X is in some clopen Lindelof set. But it still does not show that the whole space can be partitioned into these sets. I.e., starting with some x one constructs L = ⋃ n L n clopen Lindelof. Then one takes a z ∉ L and repeat the construction to get a clopen Lindelof set M = ⋃ n M n $ around z . But it could be that M intersects L . Need to think more on this.

Corollary 1 is valid no matter what, but it would be good to prove the theorem also.

@yhx-12243 fyi

Yeah, I get the issue with my proof, and I fixed it, the theorem is still true in the exact same form. Thanks

[Moniker1998]

In any case, I think it would be useful to edit the post to use this convention, i.e. rename "locally compact" to "weakly locally compact" and "locally Lindelöf" to "weakly locally Lindelöf" in your answer. That will keep things clear, and will match with what will be in pi-base eventually.

I don't think thats really necessary, naming conventions don't always have to agree with each other.

[Moniker1998]

But as for many "local properties", there are different variants, depending on whether one requires a local base of nbhds with the property around each point, or just one nbhd with the property around each point. Both notions are useful.
See https://github.com/pi-base/data/wiki/Conventions-and-Style#local-properties for the general convention used in pi-base to distinguish between the two.

Of course there are more than just two notions of locally compact space, and same should be true for locally Lindeof (I always found that strange in pi-base...). Moreover I don't think its necessary to accept two new definitions, one of them won't be used then it seems.

[prabau]

Nice fix to the proof. Thanks.

[prabau]

Nice consequence: will be able to derive that two more spaces, including S153 (Open long ray), is not para-Lindelof.

[prabau]

Looks good overall. I'll make a final suggestion to explain what is meant by the term used here that is not yet in pi-base, and to follow the pi-base convention.