Property Suggestion: Has closed discrete subset of size 𝔠

[yhx-12243]

Property Suggestion

A space is said to be「Has closed discrete subset of size 𝔠」if there does exists a closed discrete subset of cardinality 𝔠.

Rationale

The main purpose of this property is to utilize following two theorem:
(Jones) Every separable normal space is not「Has closed discrete subset of size 𝔠」.
(Engelking 5.2.C(b)) Every separable countably paracompact space is「Has closed discrete subset of size 𝔠」.

Relationship to other properties

Compare with Has a closed point (P107), Weakly countably compact (P21), and Has countable extent (P198), namely 𝑒(𝑋) > 0, 𝑒(𝑋) < ℵ₀, 𝑒(𝑋) ≤ ℵ₀, respectively.

Former discussion: #1398 (comment)

Preliminary Plan

These property will process with at least two PR's:

1. Add property and 5 theorems:
   a. Cardinality < 𝔠 ⇒ ~Has closed discrete subset of size 𝔠
   b. ~Has closed discrete subset of size 𝔠 ∧ Discrete ⇒ Cardinality < 𝔠
   c. Has countable extent ⇒ ~Has closed discrete subset of size 𝔠
   d. Separable + Normal ⇒ ~Has closed discrete subset of size 𝔠
   e. Separable + Countably paracompact ⇒ ~Has closed discrete subset of size 𝔠
   It is to be determined that (d) and (e) should be done in first PR, or split into two PR's.
2. Move the traits/assertion of related space with this property.

[Moniker1998]

Those are theorems of the form "X => P" where P is your property. Are there any theorems which use that a space is P?

It does seem like a good property to add though, under CH it would imply countable extent.
Any intermediate theorems of the form " $e(X)&lt;\mathfrak{c}\land M\implies e(X)\leq\aleph_0$ " for some property $M$?

[yhx-12243]

I've not found such famous theorem using P as a condition.

My reason is to add Separable + {Normal, Countably paracompact} ⇒ Extent < 𝔠 because this argument appears at a bunch of trait assertion.

It does seem like a good property to add though, under CH it would imply countable extent.

However we already have a property 「Cardinality < 𝔠」.

[prabau]

The main benefit I see for this property is that it allows to have Jones' lemma as a pi-base theorem.

We can then use that to replace the fact that some spaces are not normal with something easier to check, namely Extent $&lt;\mathfrak c$. For example for the Niemitzski plane, etc. (actually, it seems that that space does not prove non-normality directly).

So there are many useful results of the form [ ~P => X ] (the contrapositive of (something implies P)).

[Moniker1998]

The main benefit I see for this property is that it allows to have Jones' lemma as a pi-base theorem.

Ah, right. That is useful.

By the way, Jones' lemma exploits that closed discrete subsets are $C$-embedded (previously I said $z$-embedded but I'm not sure if that can work). Any spaces which you know for which this is true?

Namely, if this is the case, and $D\subseteq X$ is closed discrete of size $\mathfrak{c}$, then there is $2^\mathfrak{c}$ continuous $f:D\to [0, 1]$ while there is $\leq \mathfrak{c}$ continuous functions on $X$, contradiction.

[prabau]

Note one subtlety. Extent is defined as the supremum of the size of closed discrete subsets. But the sup is not necessarily a max, ie., it need not be attained.

So Engelking 5.2.C(b) for example does not say Extent $&lt;\mathfrak c$. It says each closed discrete subset has cardinality less than the continuum. But it could still be possible that the extent = continuum.

We need to look at what Jones' lemma says exactly, and if there is a problem or not.
Does the property need to be refined?

[yhx-12243]

This is indeed a tough point. Because at some strange set theory axioms, a space with extent = 𝔠 may not have continuum-sized closed discrete subset.

[Moniker1998]

Suppose that $X$ has extent $\mathfrak{c}$. We get $2^{&lt;\mathfrak{c}}$ continuous functions. Question is if $\mathfrak{c} &lt; 2^{&lt;\mathfrak{c}}$. My guess it that this inequality can fail. We do get $\leq$ though.

[Moniker1998]

Based on the discussion I've changed the name of this property (I've also checked claim of Engelking to make sure this is what being said - it is).

[prabau]

Yeah, that's much more manageable.

[prabau]

And here is an equivalent formulation for the definition:
"Has a closed discrete subset of size $\ge\mathfrak c$ "