Frechet Urysohn + Weakly First Countable + US => First countable

[felixpernegger]

The proof is the paper I cited is not correct as I mention in the PR. But it except for requiring US (giving $U$ open), it works completely, so I dont think we need to write it down again?

Also added metaproperty for WFC (intersect weak base $V$ with subspace to get $V'$. Clearly topology induced by this is not coarser than normal subspace topology, for converse suppose $Z \subseteq Y \subseteq X$ is open wrt weak basis in $Y$, then for each $x$ in $Z$ take $n$ big enough such that $V_n(x) \subseteq Y$ and $V'_n(x)\subseteq Z$, then clearly $V_n(x)\subseteq Z$, so $Z$ is open in $X$)

[prabau]

Siwiec says in section 1.7 "The Hausdorff axiom will be assumed in all that follows."
So it's not that the author erroneously does not require US; he assumes even more. We should rephrase something.

[yhx-12243]

US suffices for this statement. The proof is same as T628.

[prabau]

I know US is sufficient. What I am saying is that we need to rephrase the justification to something like:
"the author makes the blanket assumption that spaces are Hausdorff (see section 1.7), but it is sufficient to assume US."
or something like that.

[prabau]

Siwiec Prop. 1.9 mentions that P228 is hereditary wrt closed sets. Can you check if it's easy to see? If so, we could add that metaprop. as well.

[yhx-12243]

Yes it is. Just like P104, is open or closed hereditary (not marked in pi-base).

[prabau]

Yeah, we can add the same metaprops to P104 (symmetrizable).

[prabau]

Your last version looks good. Just one minor formatting suggestion below, so that the general fact is standalone.

[prabau]

Everything looks good to me. Leaving it to @yhx-12243 to approve.

[prabau]

Approving