Toronto spaces definition + easy properties

[felixpernegger]

Following the plan at the old PR (comment).

Since I think it has been established Toronto spaces are a nice property, and all theorems here are trivial, I think this PR should be uncontroversial now. Once this is merged I will make another PR some more complicated properties.

[felixpernegger]

If there are more trivial theorems (like the one with cut point) it might be good to mention them now

[prabau]

Love the choice of branch name :-)

[prabau]

T813 [Toronto + cut point => finite ]

We have many theorems where one of the properties is a kind of triviality condition. In the context of Toronto spaces, finite spaces are the trivial case. Theorems involving many properties can be phrased as: a bunch of properties imply the trivial case. But it is often more natural to move things around and put a non-triviality condition in the hypotheses. Compare for example: https://topology.pi-base.org/theorems/T000134 or https://topology.pi-base.org/theorems/T000702.

Anyway, all this to say it would be more natural to me to phrase it has "Infinite Toronto spaces don't have cut points."
i.e., [Toronto + ~finite => ~has cut point ]

[felixpernegger]

Alright that makes sense. I thought it's preferable to have as few negations as possible (for aesthetics)

[yhx-12243]

Another suggestion: When you choose (theorem) number you might simply look up the existing PR to check whether the former number are occupied.
Usually when you see “holes” (e.g., T805, T806, T811, T813) in current pi-base, basically there are PR already using the number but not merged yet.
Otherwise once this PR merged, it causes lot of PR should change number.

[felixpernegger]

Another suggestion: When you choose (theorem) number you might simply look up the existing PR to check whether the former number are occupied. Usually when you see “holes” (e.g., T805, T806, T811, T813) in current pi-base, basically there are PR already using the number but not merged yet. Otherwise once this PR merged, it causes lot of PR should change number.

ok thanks

[prabau]

I have no more comment. Leaving it to @yhx-12243 to approve.