Small fixes for P244 pi-character

[prabau]

Continuation of #1788.

Fixed a few minor things. Specifically, the confusion in P244 between $p$ and $x$. Also added a specific page for the definition.
And some clarification and tightening of the definition (I hope).

@JSMassmann Hope you can review this. Please don't do any merging before discussing first.

[prabau]

Also, is T901 (weakly first countable => countable pi-character) even correct? The $V_n(x)$ are not open sets in general.

[prabau]

@felixpernegger Please don't approve this. Let @JSMassmann do the driving for this PR.

[JSMassmann]

Sure, I don't see anything wrong with these two commits.

Regarding that last comment, that's a good point, indeed the theorem is probably false but I don't have the brainpower to come up with a counterexample right now. (If I do, maybe I'll add it in another PR.) @felixpernegger wrote that theorem and I didn't bother to carefully scrutinize it, my bad.

[prabau]

Ok, I'll remove it in this PR for now. @felixpernegger ok with you?

[prabau]

@JSMassmann I also replaced $\pi_\chi(X)$ with $\pi\chi(X)$. I assume the first one was not intentional?

[prabau]

I removed T901. If it turns out we were mistaken, it can be put back later.

[prabau]

@JSMassmann You can approve the PR is you don't have any issues. Please don't merge it yet, as I will need to tell something about that step.

[prabau]

Actually, wait. I should replace T901 with (first countable => countable pi-character).

[felixpernegger]

Also, is T901 (weakly first countable => countable pi-character) even correct? The V n ( x ) are not open sets in general.

I forgot about the open condition, sorry

[prabau]

@JSMassmann For merging to the main branch, we use "squash and merge".

Important: When you click on that button, two fields appear: "Commit message" at the top and "Extended description". Before clicking "Confirm squash and merge", we normally blank out the whole extended description field, only keeping the "commit message" field. This ensures the git log is "clean".

Please take a look at the following for an explanation:
#912 (comment) and the following comment,
and #779 (comment).

Note also that sometimes we may need to edit the "commit message" field if it is not descriptive enough. (I think that sometimes if the PR has a single commit, that commit is taken as the message, instead of the PR title, which is usually more informative.) See #1557 (comment).