Hereditarily connected => alpha_i

[felixpernegger]

You can use the same argument as for order topologies which we had earlier.
This doesnt actually give any new traits, but is not in the engnine, so why not..

[prabau]

I think it would be hard for someone to guess what "use the argument above the preorder induced by the property" means exactly. Which preorder? Which property? And where above the preorder? ...

Also, do you mind explaining here how that works?

[felixpernegger]

Hm yeah probably I should write this clearer. Will do tomorrow or next week!

[felixpernegger]

I added the proof.

[prabau]

Can you please fix "use the argument above the preorder induced by the property" in your post? That sentence is grammatically incorrect and makes no sense.
Also, you have the wrong link for "hereditarily connected".

[felixpernegger]

fixed it

[felixpernegger]

Actually I think this can be generalised to Well-based => $\alpha_1$ (technically strenghening T748, but the proof of the new theorem would depends on that). I'll change my comment accordingly. This gives 4 new traits