pi-base
Improvements to #615
Some comments for you and Jocelyn to discuss.
S154/P187: "non-trivial sequence" is not clear and seemingly not right. You probably meant a sequence of all distinct elements instead.
T473: "Asserted on page 340 ...": It would be more helpful to mention Theorem 3.2 instead (as it not only asserts, but has the proof as well (even if the proof is obvious in this case)).
The paper mentions on p. 340 the result [separable + W-space ==> first countable], which would be good have as it would imply various additional spaces are not W-space by contrapositive. But where is that shown in the paper? I couldn't see it.
Various theorems here invoke the notion of proximal space (P76). The definition of proximal space in pi-base is a little short on information though, and it would be good if you guys could expand it as needed. In particular, add J. Bell's paper as a reference, clarify whether pi-base assume Hausdorff or not (I think we discussed before that pi-base did not require Haudorff, but Bell's paper assumes that). A "purely topological" characterization is also mentioned from Clontz's paper. Is that something that can be written down, including the exact place in the paper?
T475: Does Lemma 6 from Bell's paper also work without the Hausdorff assumption? I assume so, but would be good to mention it explicitly.
T476: (I don't have access to Tkachuk's paper.) The abstract (combined with the zbmath review) mentions: A compact space $X$ is Corson compact if and only if it embeds in a topological group that is a W-space. However, that is stronger than saying $X$ is a W-space that embeds in a topological group. (i.e., how do you deduce one can choose the topological group itself to be a W-space?).
Originally posted by @prabau in https://github.com/pi-base/data/issues/615#issuecomment-2040969606
#714 has recently added that Sorgenfrey line is not proximal.
Related to that, it would be good to add at some point that proximal spaces are collectionwise normal (proved in Jocelyn Bell's paper). That would provide many other examples of spaces that are not proximal (but are W-space), for example the Sorgenfrey plane. (Does the proof of that use the Hausdorff property?)
But maybe more urgent would be to handle the paragraph about proximal in the issue at the top, including specifying in pi-base that we don't assume Hausdorff. Any plan on when this part would be able to be done?
