pi-base
Do we keep Path-connected => Connected?
Now we have $\sigma$-connected => connected and path-connected => $\sigma$-connected. Of course, the proof of path-connected => connected is much simpler than path-connected => $\sigma$-connected, so it is a question of keeping " $T_2\Rightarrow T_1$ ".
Like you said, it's similar to keeping [T2 ==> T1]. I am not going to push for removal, but we could discuss it in the Oct 4 zoom meeting. @StevenClontz ?
Path-connected => connected T40 still exists. I'm unsure of whether to remove or keep it, and can imagine arguments for both directions. I think I'm in favor of keeping it. It looks like @prabau is neutral or weakly in favor of keeping it, and @StevenClontz is in favor of keeping it. Not sure what @Jianing-Song's opinion is, but maybe it's at least weakly in support of removal? Was any decision met in the Oct 4 Zoom meeting?
https://github.com/orgs/pi-base/discussions/745 <- don't think it was discussed. But for housekeeping purposes (thanks @GeoffreySangston for pushing things forward there) I will close this, and anyone who wishes to revive the discussion to remove the theorem is welcome to re-open