Initial commit.

pi-base · Oct 17, 2024 · 8fba57e · 8fba57e
1 parent 69100d8
commit 8fba57e
Show file tree

Hide file tree

Showing 6 changed files with 50 additions and 0 deletions.
diff --git a/properties/P000197.md b/properties/P000197.md
@@ -0,0 +1,6 @@
+---
+uid: P000197
+name: Countable spread
+---
+
+A space in which every discrete subspace has countable cardinality.
diff --git a/properties/P000198.md b/properties/P000198.md
@@ -0,0 +1,6 @@
+---
+uid: P000198
+name: Countable extent
+---
+
+A space in which every uncountable subspace has a limit point.
diff --git a/theorems/T000559.md b/theorems/T000559.md
@@ -0,0 +1,11 @@
+---
+uid: T000559
+if:
+ and:
+ - P000197: true
+ - P000052: true
+then:
+ P000057: true
+---
+
+Follows from the definition of {P197}.
diff --git a/theorems/T000560.md b/theorems/T000560.md
@@ -0,0 +1,9 @@
+---
+uid: T000560
+if:
+ P000131: true
+then:
+ P000197: true
+---
+
+Follows as Lindelöf discrete spaces are countable.
diff --git a/theorems/T000561.md b/theorems/T000561.md
@@ -0,0 +1,9 @@
+---
+uid: T000561
+if:
+ P000180: true
+then:
+ P000197: true
+---
+
+Follows as separable discrete spaces are countable.
diff --git a/theorems/T000562.md b/theorems/T000562.md
@@ -0,0 +1,9 @@
+---
+uid: T000561
+if:
+ P000198: true
+then:
+ P000197: true
+---
+
+Follows as every uncountable subspace has a point that isn't isolated.