Has closed discrete subset of size 𝔠 (part 3)

[yhx-12243]

Continuation of #1584 and #1592.

Add one theorem about countably paracompactness.

Further plan:
(Last) Part 4: S101|P227 and S1103|P227

[Moniker1998]

Isn't this just one author?

[prabau]

I agree. You can use (N. Kemoto) for the author.

[Moniker1998]

I read the proof by Kemoto. There's lots of confusion between $F$ and $D$. The above passage should be disregarded completely.

[prabau]

T309: what would you think of renumbering the thm to T000838, so that it appear together with another thm with the same hypotheses in the list for https://topology.pi-base.org/properties/P000227 ? Easier to group things together.

[yhx-12243]

T309: what would you think of renumbering the thm to T000838, so that it appear together with another thm with the same hypotheses in the list for https://topology.pi-base.org/properties/P000227 ? Easier to group things together.

#1592 (comment)

@Moniker1998 he suggested.

[prabau]

I know he suggested it. But it's perfectly fine to leave a gap. It will be filled by later PRs.

[Moniker1998]

@prabau why do we need a gap

[prabau]

We don't want to have gaps long term, but they don't need to be filled immediately. It does not hurt anything in the mean time. That gap can be filled in the future by some later PR when a new theorem gets introduced.

[Moniker1998]

@prabau you didn't answer my question though. Why do we need a gap? Because satisfying our compulsions doesn't seem like a reason good enough

[prabau]

The web page of any of the properties presents the list of related theorems. For people getting familiar with a property, it is preferable to list the trivial or simple theorems first, so that one can quickly understand relations with some other properties, and then the more difficult ones.

(There is nothing absolute about that, but once a PR is merged, one should not change the numbering of theorems. So before merging, if it is feasible, one can choose a better ordering as it does not cost anything.)

The current list of theorems for P227 (discrete closed set of size continuum) looks like this:

T309 is in the category of more difficult result. And furthermore, it has the same hypotheses at T836, so if they were together, that would be an even better presentation.

I'll illustrate.

[prabau]

After the reshuffling:

[Moniker1998]

@prabau theorems list isn't dependent on individual properties... also we haven't agreed on any decision, yet you changed the numbering of this theorem.

What's a better practice, tell me. To fill in the gaps as to not forget about that there is a gap in the first place, or to worry about the ordering, which is ultimately immaterial. I'm sure nobody thinks about this as exposition to anything.

[prabau]

If someone does not care about the order of theorems, that should not prevent others from caring.

Anyway, no need to worry too much about this. It happened accidentally due to #1596 being merged just before this one, which created a gap. One can imagine #1596 has not been merged yet, and will be virtually merged as soon as this one is done.

As for filling the gaps, it's really not a big problem. When I write a PR with new theorems or spaces or properties, I always check if there are gaps and try to fill them if that makes sense compared with the numbering of other items. The current gaps for theorems are 309 and 774-777 (not sure why that last range). (There are also gaps due to pending PRs, but that's expected.)

[Moniker1998]

@prabau #1426 has 774-777

If someone does not care about the order of theorems, that should not prevent others from caring.

I don't know how that supports anything here. I've asked you what a better practice is. You didn't answer, again.
I'm not preventing you from caring, but I think there are better practices, and they should be applied.
You can still care, that's immaterial of if we implement this.

As for filling the gaps, it's really not a big problem. When I write a PR with new theorems or spaces or properties, I always check if there are gaps and try to fill them if that makes sense compared with the numbering of other items. The current gaps for theorems are 309 and 774-777 (not sure why that last range). (There are also gaps due to pending PRs, but that's expected.)

I am not exactly sure how I should feel about this. While I appreciate the check, I think that has too much potential for errors.

[prabau]

One question about the mathematics. In the Kemoto proof, the sets $g^{-1}(n)$ form a discrete family of closed sets in $X$, which is countably paracompact. Why is there a locally finite collection of open sets $G_n\subseteq X$ with $g^{-1}(n)=G_n\cap F$ ?

[prabau]

It's easy after all. One considers the countably collection of all open sets $g^{-1}(n)\cup (X\setminus F)\subseteq X$. By countable paracompactness, it has a locally finite open refinement $\{G_n\}$ with $G_n\subseteq g^{-1}(n)\cup (X\setminus F)$, which implies $g^{-1}(n)=G_n\cap F$.

[prabau]

Suggested change

	See also Claim in {{zb:1116.54006}}.
	See also the Claim on page 359 of {{zb:1116.54006}}.

[prabau]

Regarding #1597 (comment), that seems needed to justify the sentence that follows. Am I missing something?

[Moniker1998]

Regarding #1597 (comment), that seems needed to justify the sentence that follows. Am I missing something?

I don't know what answer you are expecting

[prabau]

Regarding #1597 (comment), that seems needed to justify the sentence that follows. Am I missing something?

I don't know what answer you are expecting

It's just that in the previous comment you said that passage should be disregarded. But that confused me because it seems necessary to justify the sentence that follows in the proof.

[Moniker1998]

Regarding #1597 (comment), that seems needed to justify the sentence that follows. Am I missing something?

I don't know what answer you are expecting

It's just that in the previous comment you said that passage should be disregarded. But that confused me because it seems necessary to justify the sentence that follows in the proof.

I don't see how it would be confusing. After all, it only seems to you that this sentence is necessary.

[prabau]

@yhx-12243 See #1597 (comment) and #1597 (comment). What list of theorems looks better to you in this case?

[yhx-12243]

In fact T838 looks a little bit comfortable. However I've no opinion about this. Both okay for me.

[prabau]

@Moniker1998 Going back to the previous discussion, I agree that it's usually a good idea to "fill the gaps" in the item numberings, but it really does not cause a problem if it is not done immediately. Eventually the gaps get filled as it is something we, contributors to pi-base, naturally look for. So it does not seem worth codifying this in guidelines in the wiki.