Cofinite infinite space is not biconnected

[Moniker1998]

I've also thought about replacing P138 of S15 by a theorem, but since that only holds for S15 it seemed like adding additional bloat which just isn't necessary. Or at least it seems so.

Biconnected is different since it doesn't just follow from locally injectively path-connected.
Under CH this doesn't add anything new.
But if for instance in the future we add cofinite space of size $\omega_1$ (and we should), then this trait will be deduced automatically.

[felixpernegger]

Can you maybe quickly think about if this can be strenthed to infinite + noetherian implies not biconnected? Currently has no results.

Potentially related : https://math.stackexchange.com/questions/1572687/compact-connected-space-is-the-union-of-two-disjoint-connected-sets

I've also thought about replacing P138 of S15 by a theorem, but since that only holds for S15 it seemed like adding additional bloat which just isn't necessary. Or at least it seems so.

I am not entirely sure what is the consensus here, but personally I think even very small theorems are nice since they may contribute later and help the explore tab. (especially if the theorem could be strengthened again)

[felixpernegger]

cool! Maybe you can use this as the theorem instead

[Moniker1998]

I don't think so. That proof doesn't really work.

[Moniker1998]

I've figured out that if you have an infinite Noetherian biconnected space, then it has an infinite subspace for which every open set is cofinite, and then it easily follows by decomposing into two subspaces of the same size.

[Moniker1998]

@prabau see the proof of T811. I think it's correct but it will need some changes in how it's written. Maybe better for mathse?