omega+omega+1 is not Toronto

[artemetra]

Another simple trait, resolves S34|P219.

It seems like there is no ordinal space that is Toronto and not discrete (Explore), but I don't really have a good clue on how to (dis)prove that. Maybe worth looking into later.

[felixpernegger]

Another simple trait, resolves S34|P219.

It seems like there is no ordinal space that is Toronto and not discrete (Explore), but I don't really have a good clue on how to (dis)prove that. Maybe worth looking into later.

Correct me if I wrong but I think:

Given some ordinal $X§, the cardinality of successor ordinal $e$ with $e<X$ is equal to $|X|$, thus (by Toronto) homeomorphic, but each succesor ordinal is isolated, thus the space is discrete

[prabau]

@felixpernegger That seems like the right idea. So we can change this to a theorem: ordinal space + toronto => discrete.

[prabau]

@artemetra As you now have permissions, any future PRs should be done in a branch of the official repository. That will allow people to check the work more easily, by navigating to the Advanced tab of the pi-base web site and specifying the branch name. And every commit in such a branch triggers an automated build, which is very useful for catching some types of error.

So for now I'll close this PR and you can do the above in a new branch.