renumbering the theorems

theorems/T000615.md

@@ -1,9 +1,14 @@
 ---
 uid: T000615
 if:
-  P000053: true
+  and:
+  - P000110: true
+  - P000001: true
 then:
   P000102: true
+refs:
+- mathse: 5041858
+  name: Is every developable space semimetrizable?
 ---
 
-Every metric is a semi-metric.
+See {{mathse:5041858}}.

theorems/T000711.md

@@ -4,11 +4,9 @@ if:
   P000110: true
 then:
   P000135: true
+refs:
+- mathse: 5041859
+  name: Answer to "Is every developable space semimetrizable?"
 ---
 
-Let $x,y\in X$ and let $U$ be an open set such that $x\in U$ and $y\notin U$.
-If $(\mathscr U_n)_{n\ge 1}$ is a development for $X$,
-there is some $n$ such that $\operatorname{st}(x,\mathscr U_n)\subseteq U$,
-and therefore $y\notin\operatorname{st}(x,\mathscr U_n)$.
-Thus no member of $\mathscr U_n$ contains both $x$ and $y$.
-Any open set $V\in\mathscr U_n$ with $y\in V$ will then satisfy $x\notin V$.
+See Lemma in {{mathse:5041859}}.

theorems/T000712.md

@@ -1,12 +1,9 @@
 ---
 uid: T000712
 if:
-  and:
-  - P000110: true
-  - P000002: true
+  P000121: true
 then:
-  P000102: true
+  P000110: true
 ---
 
-writing mathse post ...
-
+Letting $\mathscr U_n$ be the collection of all open balls of radius $1/n$ gives a development for $X$.

theorems/T000713.md

@@ -1,9 +1,22 @@
 ---
 uid: T000713
 if:
-  P000121: true
+  and:
+  - P000088: true
+  - P000110: true
 then:
-  P000110: true
+  P000121: true
+refs:
+  - zb: "0684.54001"
+    name: General Topology (Engelking, 1989)
 ---
 
-Letting $\mathscr U_n$ be the collection of all open balls of radius $1/n$ gives a development for $X$.
+This is essentially one of Bing's metrization theorems.
+
+Suppose $X$ satisfies the hypotheses.
+Since {T711}, we can add {P135} to the hypotheses.
+
+Passing to the Kolmogorov quotient, it is equivalent to show that
+{P88} {P110} {P2} spaces are {P53}.
+This is exactly Theorem 5.4.1 in {{zb:0684.54001}},
+which assumes {P2} as part of the definition of {P88}.

theorems/T000714.md

@@ -2,21 +2,13 @@
 uid: T000714
 if:
   and:
-  - P000088: true
+  - P000018: true
   - P000110: true
 then:
-  P000121: true
+  P000027: true
 refs:
-  - zb: "0684.54001"
-    name: General Topology (Engelking, 1989)
+  - mathse: 148565
+    name: Lindelof developable spaces are second countable
 ---
 
-This is essentially one of Bing's metrization theorems.
-
-Suppose $X$ satisfies the hypotheses.
-Since {T711}, we can add {P135} to the hypotheses.
-
-Passing to the Kolmogorov quotient, it is equivalent to show that
-{P88} {P110} {P2} spaces are {P53}.
-This is exactly Theorem 5.4.1 in {{zb:0684.54001}},
-which assumes {P2} as part of the definition of {P88}.
+See {{mathse:148565}}.

theorems/T000715.md

@@ -1,14 +1,9 @@
 ---
 uid: T000715
 if:
-  and:
-  - P000018: true
-  - P000110: true
+  P000113: true
 then:
-  P000027: true
-refs:
-  - mathse: 148565
-    name: Lindelof developable spaces are second countable
+  P000110: true
 ---
 
-See {{mathse:148565}}.
+By definition.

theorems/T000716.md

@@ -3,7 +3,7 @@ uid: T000716
 if:
   P000113: true
 then:
-  P000110: true
+  P000005: true
 ---
 
 By definition.

theorems/T000717.md

@@ -1,9 +1,11 @@
 ---
 uid: T000717
 if:
-  P000113: true
+  and:
+  - P000110: true
+  - P000005: true
 then:
-  P000005: true
+  P000113: true
 ---
 
 By definition.