Initial PR for countable pi-weight/pi-character

[JSMassmann]

I added "Has countable $\pi$-weight" and "Has countable $\pi$-character" and the fact that the former implies the latter and separability.

See #1712

[felixpernegger]

This is a good PR. However P243 and P244 are now only have theorems in one direction, i.e. the deduction engine will not yet show some space does in fact have one of these properties.

So I suggest adding (in this PR) the following easy theorem:

• Second countable => Has countable pi weight
• Weakly first countable => Has countable $pi$ character

[felixpernegger]

What does "NB" means? I would either remove that sentence or write "Note: ..." instead

[JSMassmann]

NB = Nota bene = "note well", used to draw the reader's attention to a detail. I suppose one could replace it with just "Note".

[prabau]

This is a good PR. However P243 and P244 are now only have theorems in one direction, i.e. the deduction engine will not yet show some space does in fact have one of these properties.

So I suggest adding (in this PR) the following easy theorem:
...

@felixpernegger the fact that this is barebones is intentional, as @JSMassmann is a new contributor and without full permissions yet (the main goal at this point is to show the recommended procedures). See #1712 (comment).

So let's keep it as it is for now.

[prabau]

@JSMassmann the title of the PR should be informative, so we can see at a glance what each PR is about when looking at the list of PRs. "Initial PR for pi-base-related properties" is completely non-informative. Can you change it to something like "pi-weight and pi-character properties" for example?

Added later: Apologies, I realized I misinterpreted "pi-base" to mean the pi-base platform. Anyway, my suggested change seems less ambiguous.

Also, when we write a PR based on a previous issue, we normally reference the issue in the summary at the top. So you can mention #1712 there.

[felixpernegger]

---
uid: T000901
if:
  P000228: true
then:
  P000244: true
---

Choose $\mathcal{V}_x := \mathcal{T_x}$.

---
uid: T000902
if:
  P000027: true
then:
  P000243: true
---

Follows since a topological base is a $\pi$-base.

Thats all you need. We shouldnt have unusuable properties at any point.

[prabau]

@felixpernegger You were not supposed to change the title of the PR yourself :) The PR author should have done it. One learns better by doing!!!

[felixpernegger]

wellll...

[JSMassmann]

Okay. <joke>I could change the PR title back, and then back again.</joke>
Should I add the two theorems that @felixpernegger just wrote to the PR, or keep it like this?