Theorem Suggestion: Connected+ strongly paracompact => countable extent

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?

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

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

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

@pzjp

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

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?

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

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?

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$.

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.

Can I add new theorem P36 + P145 => P18 ?
No other PR with new theorems is on the way, right? Who assigns the new number?

Can I add new theorem P36 + P145 => P18 ? No other PR with new theorems is on the way, right? Who assigns the new number?

Yes, please do.

For the new number, just pick the next number available (unless you can see that some other pending PR already wants to use that number). But it does not really matter if two pending PRs have a conflicting number. When that happens, the first PR that gets approved and merged gets the number, and the second one can then just change its number to avoid a conflict.

Navigation Menu

Repository navigation

Theorem Suggestion: Connected+ strongly paracompact => countable extent #1189