Toronto + not hyperconnected + finite => has an isolated point

[felixpernegger]

We discussed in #1773, the author said he would PR this, but didnt do so (and didnt react to my follow up). Since this theorem is really powerful (over 50 traits!), I PR it myself.

[prabau]

The proof looks good.

Comparing with the list of theorems for Toronto (P219), would it be possible to move P219 to be the first hypothesis of the theorem?

[prabau]

I am curious. The only infinite Toronto spaces that are not hyperconnected currently in pi-base are discrete. Are there such spaces that are not discrete?

[felixpernegger]

I am curious. The only infinite Toronto spaces that are not hyperconnected currently in pi-base are discrete. Are there such spaces that are not discrete?

Under GCH infinite T2 spaces are Toronto and we dont really have many spaces which are not hyperconnected and not t2, see https://topology.pi-base.org/spaces?q=%7EHyperconnected+%2B+%7Et2
So this might just be a coincidence

[felixpernegger]

The proof looks good.

Comparing with the list of theorems for Toronto (P219), would it be possible to move P219 to be the first hypothesis of the theorem?

I found this to be the most natural way to state it, but if you want me to change it, sure just say