S195 part 1 of missing traits

[Moniker1998]

Splitting the original PR #1486 into managable chunks and adding them because the author didn't come back

I've chosen 4 traits to add, 1 which looked more challenging, and 3 that looked easy. I haven't read them myself yet, I will notify when I do. I've also included the slight change to the README file

[Moniker1998]

@prabau checked and revised using my own words

[prabau]

README: apart from the suggestion above, I am thinking that giving the basic open sets at the end in the form $[0,\alpha]\setminus F=[0,\alpha+1)\setminus F$ instead of $[0,\alpha)\setminus F$ would be more useful, as it's easier to see what basic nbhds of $\alpha$ would be. Compare with the README for S217.

Compare also with the justification for P28 (first countable).

What's your opinion?

[prabau]

P16 (compact) is now redundant due to P24. Can be removed.

[prabau]

P84: there is a very minor problem, but we can just take $\alpha=\omega+\omega$ to simplify things.

[prabau]

For P93 above, I am using the equivalent characterization that each point has a countable nbhd. It's rather obvious. Should it be mentioned in https://topology.pi-base.org/properties/P000093 ?

[Moniker1998]

README: apart from the suggestion above, I am thinking that giving the basic open sets at the end in the form [ 0 , α ] ∖ F = [ 0 , α + 1 ) ∖ F instead of [ 0 , α ) ∖ F would be more useful, as it's easier to see what basic nbhds of α would be. Compare with the README for S217.

@prabau that's okay, I also think this will probably be better

[Moniker1998]

P16 (compact) is now redundant due to P24. Can be removed.

@prabau I will remove traits in the final part of the edits to S195

[Moniker1998]

P84: there is a very minor problem, but we can just take α = ω + ω to simplify things.

@prabau what's the problem?

[Moniker1998]

For P93 above, I am using the equivalent characterization that each point has a countable nbhd. It's rather obvious. Should it be mentioned in https://topology.pi-base.org/properties/P000093 ?

@prabau I think so, yes

[prabau]

P84: there is a very minor problem, but we can just take α = ω + ω to simplify things.

@prabau what's the problem?

"any two neighbourhoods of $\omega+\omega$ and $\omega+n$ ... , and so intersect."
But $\omega+\omega$ may not even belong to the nbhd of $\alpha$.

So need to reword something. Or easier, just focus on nbhd of $\omega+\omega$ itself and ignore the case of general $\alpha$.