Two theorems implying CWN

[prabau]

Two new theorems:

• T661: countable spread + normal => collectionwise normal
• T662: countable extent + $T_4$ => collectionwise normal

Note: this allows to derive that two more spaces don't have countable extent.

---

Also slight reformatting of P88 (collectionwise normal) to make things clearer. Among other things, added the terminology "disjoint open expansion" and "discrete open expansion" as suggested by @GeoffreySangston in #997 (comment) and subsequent comments. Feel free to comment on that part if you think it's unnecessary.

Also minor correction for https://topology.pi-base.org/spaces/S000082/properties/P000021, used to show that space has countable extent.

[prabau]

@StevenClontz The build for this branch cwn2 succeeds, but for some reason I am unable to preview it on the web site.
For some reason, the initial updating of the traits gets stuck. Any idea?

If nothing else works, I'll try to redo it in another branch.

[StevenClontz]

possibly related: pi-base/web#200 (in that case, I know I introduced an error for the Empty space, but it wasn't caught at compilation)

[prabau]

Interesting. For me, when going to the Advanced tab and trying to preview the new branch, the initial updating of all the traits (as indicated by the progress of the green bar) gets stuck half way through and it never finishes. Was that the same symptom you were having?

[GeoffreySangston]

I've had a similar issue. On chrome you can clear the cache for a single website: chrome://settings/content/all?searchSubpage=pi-base, and this may fix the issue.

[prabau]

Thanks for the tip. In this case it did not help. I'll try something else.

[yhx-12243]

Maybe it is caused by the contradiction due to your typo (... + ~Normal ⇒ CWN) and (... + $T_4$ ⇒ CWN).

However, as pi-base/web#200 said, it wasn't caught on build (yes I cloned a local copy of compiler and it wasn't report neither), nowadays we should fix the typo and resume, leave pi-base/web#200 continue.

[prabau]

@yhx-12243 Very good eyes! That must be it.

Yes, working now!

[StevenClontz]

Nicely spotted @yhx-12243!

I'm not sure what's happened that has caused the compiler to not catch these contradictions. 😢 But we'll need to be vigilant to ensure that things are working in the viewer until pi-base/web#200 can be addressed.

[prabau]

Note: It does not seem possible to generalize T662 to [countable extent + normal => collectionwise normal].

For example, take a space $Y$ that is $T_4$ but not collectionwise normal. For example S136 (Bing's Example G).
Let $X=Y\times B$, where $B$ is a two-point set with the indiscrete topology.
Then $X$ is weakly countably compact (= limit point compact) because every nonempty set has a limit point.
And it is normal, but not collectionwise normal (by looking at the Kolmogorov quotient, which is homeomorphic to $Y$).

[prabau]

@yhx-12243 How does that look now?