Has closed discrete subset of size 𝔠 (part 1) (#1584)

Author: yhx-12243

properties/P000227.md

@@ -0,0 +1,18 @@
+---
+uid: P000227
+name: Has a discrete closed set of size $\mathfrak c$
+---
+
+$X$ has a discrete closed set of cardinality $\mathfrak c=2^{\aleph_0}$.
+
+*Note*: Discrete closed sets are exactly the sets with no limit point in $X$.
+
+*Note*: This property implies $e(X)\ge\mathfrak c$,
+where the *extent* $e(X)$ is the supremum of the cardinality of discrete closed sets in $X$.
+But there are spaces with $e(X)=\mathfrak c$ and without discrete closed set of cardinality $\mathfrak c$,
+i.e., where the supremum is not attained.
+
+Compare with these properties, where $D$ denotes a discrete closed set in $X$:
+- {P107} $(\exists D: |D|=1)$
+- {P21} $(\forall D: |D|<\aleph_0)$
+- {P198} $(\forall D: |D|\le\aleph_0)$

theorems/T000067.md

@@ -5,14 +5,11 @@ if:
 then:
   P000058: true
 refs:
-- zb: "1052.54001"
-  name: General Topology (Willard)
 - wikipedia: Continuum_hypothesis
   name: Continuum hypothesis
 ---
 
-Since $|\omega| < \mathfrak{c} = 2^{\omega}$.
+Since $\aleph_0 < \mathfrak{c} = 2^{\aleph_0}$.
 
-Proven in 1.14 of {{zb:1052.54001}}. See 1.16 of the same text or
-{{wikipedia:Continuum_hypothesis}} for discussion on the independence
-of the converse from ZFC.
+----
+The converse is independent of ZFC.  It is true iff CH holds.

theorems/T000833.md

@@ -0,0 +1,12 @@
+---
+uid: T000833
+if:
+  P000227: true
+then:
+  P000198: false
+---
+
+Since $\aleph_0 < \mathfrak{c} = 2^{\aleph_0}$.
+
+----
+The converse is independent of ZFC.  It is true iff CH holds.

theorems/T000834.md

@@ -0,0 +1,9 @@
+---
+uid: T000834
+if:
+  P000227: true
+then:
+  P000058: false
+---
+
+Follows from the definitions.

theorems/T000835.md

@@ -0,0 +1,11 @@
+---
+uid: T000835
+if:
+  and:
+  - P000052: true
+  - P000058: false
+then:
+  P000227: true
+---
+
+In {P52} spaces, any subset is closed and discrete.

theorems/T000836.md

@@ -0,0 +1,14 @@
+---
+uid: T000836
+if:
+  and:
+  - P000026: true
+  - P000227: true
+then:
+  P000013: false
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
+---
+
+Jones' lemma, see Corollary 2.10 in {{zb:0684.54001}}.