Add LOTS+(path-)connected => locally (path-)connected

[Jianing-Song]

Per issue #727 , I'm opening a PR concerning the two most basic are closely-related facts: LOTS+(path-)connected => locally (path-)connected.

I wanted to cite Munkres's Topology, bacause Theorem 24.1 mentions the result used in {T522}, and Theorem 24.3 is the intermediate value theorem used in {T523}. I'm not sure about the correct way to cite it, so thank you for your help :)

[prabau]

Do you mind closing this PR and redoing it on a branch forked from the main pi-base repo, so we can examine it and interact with it on the web site?

[prabau]

Also, can you please only include your proposed T522 in the new PR?

We can discuss T523 later separately after T522 is approved.

[StevenClontz]

(just confirming that @Jianing-Song is an approved maintainer and has the ability to create branches on pi-base/data directly)

[prabau]

For quoting Munkres, you can search for "Munkres" in github.dev for example and that will give you examples that use it. For example, see https://topology.pi-base.org/spaces/S000153/references.

That tells you Munkres is zb: "0951.54001", which you can add to the refs: section. Then in the text you can just use something like ... Theorem 24.1 in {{zb:0951.54001}} ...

[Jianing-Song]

For quoting Munkres, you can search for "Munkres" in github.dev for example and that will give you examples that use it. For example, see https://topology.pi-base.org/spaces/S000153/references.

That tells you Munkres is zb: "0951.54001", which you can add to the refs: section. Then in the text you can just use something like ... Theorem 24.1 in {{zb:0951.54001}} ...

Thanks! I have reopened this PR as #731 .