P182: Has a countable network (#571)

properties/P000182.md

@@ -0,0 +1,13 @@
+---
+uid: P000182
+name: Has a countable network
+refs:
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
+---
+
+A space with a (finite or infinite) countable network.
+
+A family $\mathcal N$ of subsets of $X$ is called a *network* if every open set is the union of a subfamily of $\mathcal N$.  That is, for every open set $U$ and point $x\in U$ there is some $A\in\mathcal N$ with $x\in A\subseteq U$.
+
+Defined on page 127 of {{mr:1039321}}.

theorems/T000093.md

@@ -1,9 +1,14 @@
 ---
 uid: T000093
 if:
-  P000057: true
+  P000182: true
 then:
   P000180: true
+refs:
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
 ---
 
-Every subset of a {P57} space is {P57}, hence {P26}.
+Having a countable network is a hereditary property; and a space with a countable network is {P26}, since choosing one point from each element of the network provides a dense set in $X$.
+
+See page 127 and the diagram on page 225 in {{mr:1039321}}.

theorems/T000259.md

@@ -3,10 +3,12 @@ uid: T000259
 if:
   P000057: true
 then:
-  P000131: true
+  P000182: true
 refs:
-  - wikipedia: Lindelöf_space
-    name: Lindelöf space
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
 ---
 
-Being countable is a hereditary property, and countable implies Lindelöf by {T74} and {T122}.
+Evident, as the collection of all singletons in $X$ is a network.
+
+See page 127 and the diagram on page 225 in {{mr:1039321}}.

theorems/T000260.md

@@ -1,12 +1,14 @@
 ---
 uid: T000260
 if:
-  P000027: true
+  P000182: true
 then:
   P000131: true
 refs:
-  - mr: 2048350
-    name: General Topology (Willard)
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
 ---
 
-Being second countable is a hereditary property, and second countable implies Lindelöf by 16.9 in {{mr:2048350}}.
+Having a countable network is a hereditary property; and a space with a countable network is {P18}, as shown for example in Theorem 3.8.12 of {{mr:1039321}}.
+
+See also the diagram on page 225 in {{mr:1039321}}.

theorems/T000271.md

@@ -3,12 +3,12 @@ uid: T000271
 if:
   P000027: true
 then:
-  P000180: true
+  P000182: true
 refs:
-- mr: 2048350
-  name: General Topology (Willard)
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
 ---
 
-Let $\{U_n\}$ be a countable basis for $X$, and $S\subseteq X$.  For each $n \in \omega$ for which $S\cap U_n\neq \emptyset$, choose $x_n \in S\cap U_n$. Then $\{x_n\}$ is a countable dense subset of $S$.
+Evident, as a base for the topology is a network.
 
-See 16.9 of {{mr:2048350}}.
+See page 127 and the diagram on page 225 in {{mr:1039321}}.

theorems/T000334.md

@@ -0,0 +1,14 @@
+---
+uid: T000334
+if:
+  and:
+    - P000182: true
+    - P000001: true
+then:
+  P000163: true
+refs:
+  - mr: 1039321
+    name: General Topology (Engelking, 1989)
+---
+
+See page 127 in {{mr:1039321}}.