diff --git a/properties/P000197.md b/properties/P000197.md new file mode 100644 index 000000000..198912435 --- /dev/null +++ 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 new file mode 100644 index 000000000..f5b0f3af9 --- /dev/null +++ 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 new file mode 100644 index 000000000..d385122ac --- /dev/null +++ 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}. \ No newline at end of file diff --git a/theorems/T000560.md b/theorems/T000560.md new file mode 100644 index 000000000..a339854dc --- /dev/null +++ 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 new file mode 100644 index 000000000..3779eb651 --- /dev/null +++ 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 new file mode 100644 index 000000000..5c91efd48 --- /dev/null +++ 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.