Theorem Suggestion: Connected+ strongly paracompact => countable extent

[pzjp]

Theorem Suggestion

If a space is:

• connected P36
• strongly paracompact P145

then it has countable extent P198.

Rationale

This theorem would demonstrate that no spaces satisfy the following search:
https://topology.pi-base.org/spaces?q=connected%2BStrongly+paracompact%2B%7EHas+countable+extent
Would also (eventually) resolve P145 for S129 and S134.

Proof

Let $C$ be a closed discrete subspace of a connected and strongly paracompact space $X$. Take an open cover $\mathscr U=\{X\setminus A\}\cup\{U_a:a\in C\}$ where $U_a$'s are disjoint open neighborhoods of the elements of $C$. Let $\mathscr A$ be a star-finite refinement of $\mathscr U$ and for every $a\in C$ fix $E_a\in \mathscr A$ such that $a\in E_a$. Clealry, $E_a\neq E_b$ for distinct $a,b\in C$.
Consider a graph $G=\{ \mathscr A, E\}$ where $(U,V)\in E$ whenever $U\neq V$ and $U\cap V\neq \emptyset$. By the connectedness of $X$ and the fact that $\mathscr A$ is an open cover, $G$ is a connected graph and by star-finiteness every vertex is of finite degree.
A connected graph with all vertices of finite degree has to be countable (there are finitely many vertices at a distance at most $n$ from the given one and the graph is a countable union over all distances). Hence $C$ is countable as well.

Should I make a self-answered entry on MathSE for this?

[yhx-12243]

Nice! Resolves the counterexample of converse of P145 (Strongly paracompact) ⇒ P30 (Paracompact).

[pzjp]

I'm currently working on S129 and that's how I landed here.

[yhx-12243]

#990 has some partial results on S129 that you can refer to.

[yhx-12243]

The results can be strengthen to P18 (Lindelöf), https://mathoverflow.net/questions/433812/a-stronger-version-of-paracompactness is also a good reference. @pzjp

[pzjp]

True. It appears that every star-finite open cover of a connected space has to be (at most) countable.
Maybe I should post my proof at mathoverflow?

[yhx-12243]

Yes you can post it right after that existing post (if you think the current answer is not complete)

[prabau]

It would be good to have the "metric hedgehog" (as mentioned by Tyrone in comment to the mo post) as a space in pi-base. That's essentially the quotient of S129 (Wheel without its hub) obtained by collapsing the outer circle to a point.
That would be another example of paracompact and not strongly paracompact space, for basically the same reason.

We should have both:

• Metric hedgehog with countably many spines
• Metric hedgehog with uncountably many spines

I am guessing the first one would be strongly paracompact.

Now I am looking at S134 (Radial metric on the plane). Isn't that the same as the (second) metric hedgehog?

[yhx-12243]

The second is exactly S134. The first is embeddable in Euclidean plane $\mathbb R^2$ by $(r, \theta)$ with $0 \leq r \leq 1$ and $\theta = \dfrac 1n$.

[prabau]

If anyone of us plans to add one or more hedgehog spaces, I think it would be good to first create an issue to discuss the best presentation to choose for pi-base, which versions to add, names and so on.