An update to double origin plane (S66)

[pzjp]

Most of missing traits, zbMath references and cleanup.

I guess strongly zero dimensional will be resolved by a theorem in the future (I suppose strongly 0-dim + Hausdorff => totally path disconnected).

To my understanding the space is not simply connected (the fundamental group should be $\mathbb Z$) but I am not that confident about algebraic topology to write the proof down (I guess one can find a universal cover for it, but it would be a bit odd space).

[yhx-12243]

To my understanding the space is not simply connected (the fundamental group should be 𝑍) but I am not that confident about algebraic topology to write the proof down (I guess one can find a universal cover for it, but it would be a bit odd space).

P200 (Simply connected): I will propose a PR about S51 (Khalimsky line) and S213 (pseudocircle) to prove this, see #1422, maybe I will resolve S66|P200 in that PR (construct a continuous map from S66 to S213, and it induce a homomorphism between their fund. groups).

[yhx-12243]

I guess strongly zero dimensional will be resolved by a theorem in the future (I suppose strongly 0-dim + Hausdorff => totally path disconnected).

P217 (Strongly zero-dimensional): already resolved by T400 of #1414, if you merge main branch.

[Moniker1998]

@yhx-12243 how do you see it on a graph like that?

[yhx-12243]

@yhx-12243 how do you see it on a graph like that?

See pi-base/web#81.

[Moniker1998]

@yhx-12243 hmm... thanks. How would you actually apply it though? Do you need to download main web, merge graph into main, then download the data?

[yhx-12243]

@yhx-12243 hmm... thanks. How would you actually apply it though? Do you need to download main web, merge graph into main, then download the data?

Roughly yes, by deploying it at my local machine/server.