Circles and rationals are not Toronto

[artemetra]

First time contributing, two easy traits. These spaces are not Toronto:

• S000170 Circle S^1
• S000027 Rational numbers Q

Let me know if something is wrong here, I'll gladly fix it.

[prabau]

Hi @artemetra Thanks for your interest in pi-base. Regarding the Toronto property, PR #1549 has been proposed in the past to add various theorems that would allow to deduce more traits automatically. But that PR is on hold and pieces of it need to be broken off into their own little PR. You can read the whole discussion about it.
So the two traits you are proposing would most probably become redundant and we would rather focus on some of the pending theorems instead.

@felixpernegger Is there anything you'd like to add?

[prabau]

I have not looked in detail at the proposed theorems in #1549, but here is one simple theorem that would cover your two spaces:
[ T2 + no isolated point => not Toronto ]

Maybe @felixpernegger has a better one that covers even more.