Some traits for S174

[felixpernegger]

This PR has low priority!

[felixpernegger]

Just to make clear this contains MORE that just the subspaces as in the newer PRs

[Moniker1998]

@felixpernegger can you delete ~P58 and P163 and add P65

[Moniker1998]

This is not trivial enough to just assert this as facts. One needs an elaboration. Clearly sets of the form $\{\omega\}^n\times (\omega+1)^\omega$ form a clopen base for this point, so it's enough to show that they're not compact. And this follows because it has topology larger than that of the product topology if $\omega+1$ were given discrete topology, which is not compact.

[Moniker1998]

Replace with not P62

[Moniker1998]

Suggested change

	The point $p := (0, 0, \dots) \in X$ is isolated via $\{p\} = 0 ^ \omega \cap \omega_1 ^ \omega$.
	The point $p := (0, 0, \dots) \in X$ is isolated since $\{p\} = 1^\omega$ where $1 = \{0\}$.

[Moniker1998]

Suggested change

	The subspace $2 ^ \omega \setminus \{(0,0,\dots)\} \subseteq X$ has no isolated point.
	The subspace $2 ^ \omega \setminus \{(0,0,\dots)\} \subseteq X$ is homeomorphic to Cantor set without a point, and so has no isolated points.

[Moniker1998]

Replace with not P62

[Moniker1998]

@felixpernegger so I've figured out that Pol, in proposition 2, actually proves a lot more than just lack of paracompactness.

Namely, this argument works to show Pol's space is not weakly $\delta\theta$-refinable space. In such space, a locally countable collection is $\sigma$-discrete. See theorem 13.3 of Borel measures by Gardner and Pfeffer in Handbook of set-theoretic topology

In particular, we can add that Pol's space is not meta-Lindelof, and not submetacompact.

[Moniker1998]

It's not weakly Lindelof, since the cover by sets $\xi^\omega$ for $\xi\in\omega_1$, a countable subcollection would be some set of the form $\xi^\omega$, and it's closed, so not dense.

Easy argument, gets rid of two properties you wanted to add.

[Moniker1998]

@felixpernegger