Discrete space of size $2 ^ \mathfrak{c}$

[felixpernegger]

The main point of this is to have a space which does not have less or equal continuum density (P209).
Also added a trivial theorem related to this.

(Ive been going over unknown implications more or less systematically and this would clear a lot for example. Adding this space would remove the pairs of properties (PA,PB) where we dont automaticallly know if there is an impication or not by 1/5 or so)

[prabau]

Your gave this PR the title "Discrete space of size $2^\mathfrak c$". This seems a great name for this space, better than "Discrete topology on $2^\mathfrak c$".

Also, the README says "Let $X=2^{\mathfrak c}$ be the power set of the real numbers", treating $2^{\mathfrak c}$ as a specific set. But in the justifications for cardinality, $2^{\mathfrak c}$ is treated as a cardinal instead.
How about we write things more consistently as:
Let $X$ be a set of size $2^{\mathfrak c}$, for example the power set of the real numbers, ...

---

As for the other discrete spaces, specifically the infinite ones, they were called "Discrete topology on ..." to mimic the entry name in S&S. One could possible change the main name to:

• S2: Discrete space of size $\aleph_0$
• S3: Discrete space of size $\mathfrak c$

On the other hand, the sets $\omega$ and $\mathbb R$ are rather canonical, so keeping the names as is seems like it would be fine too. Not sure.

Any thoughts?

(also @StevenClontz fyi)

[prabau]

Also, the numbering for spaces has a gap at S106. What about using that number instead?

[yhx-12243]

Also, the numbering for spaces has a gap at S106. What about using that number instead?

Merged into S30 homeomorphically before.

[felixpernegger]

Your gave this PR the title "Discrete space of size 2 c ". This seems a great name for this space, better than "Discrete topology on 2 c ".

Also, the README says "Let X = 2 c be the power set of the real numbers", treating 2 c as a specific set. But in the justifications for cardinality, 2 c is treated as a cardinal instead. How about we write things more consistently as: Let $X$ be a set of size $2^{\mathfrak c}$, for example the power set of the real numbers, ...

As for the other discrete spaces, specifically the infinite ones, they were called "Discrete topology on ..." to mimic the entry name in S&S. One could possible change the main name to:

* S2: Discrete space of size 
    
      ℵ
      0

* S3: Discrete space of size 
    
      c

On the other hand, the sets ω and R are rather canonical, so keeping the names as is seems like it would be fine too. Not sure.

Any thoughts?

(also @StevenClontz fyi)

I would keep it as it is (though use "discrete size of" for this PR), since its just more common, might also be better for search engine visibility...
On that note, I noticed that S2 has the alias "Countable discrete topology" which does not fit our naming conventions

[prabau]

FYI, the only reason for the alias "Countable discrete topology" for S2 is that it's the name in S&S.