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]

@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

[felixpernegger]

Sorry for the delay @Moniker1998

[Moniker1998]

@felixpernegger no problem. Also sorry for not spending time and reviewing this after you came back. I didn't feel like doing this. But I'll focus on it right now

[felixpernegger]

Yeah I have also kind of lost interest in contributing to pibase in this way for a variety of reasons.

[Moniker1998]

@felixpernegger looking at the proof of theorem 13.3. They say: "It follows from Section 3.11 in Burke's Chapter 9, that ...".
This is a bit problematic. First, section 3.11? Section is 3. And they mean lemma, but lemma 3.10 and not 3.11.
Anyway the crux is that a star-countable family can be decomposed into countable families with pairwise disjoint unions (using the "chain" trick). Then because the family $\mathcal{H}$ is an open cover of $E_n$, each of those countable families gives a family of pairwise disjoint open sets, and because each element of $\mathcal{H}$ is countable, those open sets are countable. So we can extract $E_n$ as countable union of discrete sets from this.

The proof works, but it's written a bit weirdly.