P246: Collectionwise Hausdorff

[prabau]

As proposed in #1808.

[prabau]

@JSMassmann FYI

[Moniker1998]

@prabau How do you show that if $X$ is CWH, then $Kol(X)$ is CWH? Since if $D\subseteq Kol(X)$ is closed and discrete there need not be a corresponding closed and discrete $D_0\subseteq X$ as far as I can see

[yhx-12243]

Agree. We only have Kol(X) is CWH ⇒ X is CWH. The converse is surely false since X × S4 is always CWH (¬P107 → CWH)

[JSMassmann]

Ah, thank you @prabau for doing this. I'll take a look. (My Internet connection right now isn't great, so I might not be able to talk so actively...)

[JSMassmann]

LGTM. I don't have an opinion on whether we should use P19 or P21.

[prabau]

@StevenClontz We are having a disagreement about T921 (see above) and need your opinion.

My point is that, as a general rule, if a theorem can be stated in two equivalent ways, it is preferable to use the version that uses the better known properties. Specifically, suppose the combination of properties A and B is equivalent to A' and B', and pi-base already knows that. A new theorem could be stated as either (1) A + B => C or (2) A' + B' => C. Among the two options, if one combination of hypotheses is more commonly used or more well-known, we should use that one.

(Even if the proof would be marginally shorter with one set of hypotheses, what matters more is the statement itself, which will be read and used (in traits deductions for example) countless times compared with the proof itself, which can be viewed as a black box after it is understood.)

[StevenClontz]

Personally I don't have a strong opinion about the specific situation here, and see merit in both perspectives.

In this situation where the proposal is correct, and the reviewer and proposer only disagree over style, and there's nothing in our style guide to refer to, I think it's best to approve and merge the original proposal. Of course, the reviewer is welcome to open a new PR to make their suggested change in style.

This also reminds me of a thought I had that we should probably move our style guide into the project itself. Right now anyone can edit the wiki and "declare" style conventions, but we have enough community members where our style guide really should be subject to the same peer review as any other change. (I feel like I may have even made this comment before, but never did anything about it. That should probably change.)

[prabau]

Personally I don't have a strong opinion about the specific situation here, and see merit in both perspectives.

@StevenClontz In your opinion, what is the other perspective, as I am confused about what it would be?
(Please see the latest version of T921, which does mention weakly countably compact, which is exactly what Moniker wants to see.)

[StevenClontz]

LGTM other than consideration of one suggestion.

[StevenClontz]

Personally I don't have a strong opinion about the specific situation here, and see merit in both perspectives.

@StevenClontz In your opinion, what is the other perspective, as I am confused about what it would be? (Please see the latest version of T921, which does mention weakly countably compact, which is exactly what Moniker wants to see.)

I think there are actually three non-equivalent and reasonable perspectives here:

• Theorems should choose assumptions that most naturally (by their definitions) lead to their consequence.
• Theorems should choose assumptions that make for the most natural deductions across the site.
• Theorems should choose assumptions that match what would most likely appear in the literature.

I don't feel I know offhand which is best, and don't recall if we established a convention. If we did, I didn't find it in the wiki, which is what I usually turn to.

(I reviewed the substance of the PR after my previous comment, and only saw the most recent T921 where I made my suggestion.)

[StevenClontz]

Oh, we have this: https://github.com/pi-base/data/wiki/Reviewing#requirements-for-a-new-theorem

• We like for theorems to be generalized when possible (e.g. assume regular, not $T_3$). But this
  should be considered on balance with usage in the literature (if the result is only cared about in
  the context of "assume all spaces are Hausdorff", then it's fine to have the technically weaker result).
  • Put another way, it's okay to accept a contribution of "$T_3$ and P implies Q" even when the result
    could be improved to "regular and P implies Q". But this does not mean we should reject a later
    improvement of the result to say "regular and P implies Q" if a contributor suggests doing so.

I think this lines up with my earlier take: the contributor gets to make this kind of call.

[Moniker1998]

Yeah I was too harsh with my critique, either way would be fine as long as its mentioned the two are equivalent

[prabau]

@Moniker1998 If you are satisfied with the latest version, can this be approved?

[Moniker1998]

@StevenClontz I think your change was taken care of, so I'll dismiss it

I believe this change was already taken care of