Merge branch 'main' into bettert848

felixpernegger · web-flow · commit 13ea9f80ae83 · 2026-04-12T01:47:10.000+02:00
diff --git a/properties/P000037.md b/properties/P000037.md
@@ -18,3 +18,4 @@ Compare with {P38} and {P95}.
 
 - $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.
 - This property is preserved by arbitrary products.
+- This property is preserved in any coarser topology.
diff --git a/properties/P000038.md b/properties/P000038.md
@@ -17,3 +17,8 @@ and {P95}, which requires the path to be a homeomorphism onto its image.
 Defined on page 29 of {{zb:0386.54001}} with the name "arc connected".
 Here we reserve that name for the stronger property {P95},
 which is the more common usage in the literature.
+
+#### Meta-properties
+
+- This property is preserved by arbitrary products.
+- This property is preserved in any coarser topology.
diff --git a/properties/P000223.md b/properties/P000223.md
@@ -0,0 +1,13 @@
+---
+uid: P000223
+name: Locally contractible
+refs:
+  - zb: "1044.55001"
+    name: Algebraic Topology (Hatcher)
+---
+
+$X$ admits a basis of open sets which are {P199}.
+
+Equivalently, for each $x \in X$, every neighborhood of $x$ contains a {P199} open neighborhood of $x$.
+
+"Locally contractible" is used in {{zb:1044.55001}}, where it is defined informally with the meaning above as part of the statement of Proposition A.4 on page 522.  (As explained on page 61, the book follows the convention of a space being "locally P" for a property P to mean that every point has arbitrarily small open neighborhoods with the property; this is very close to the [general convention used in pi-base](https://github.com/pi-base/data/wiki/Conventions-and-Style#Local-Properties).)
diff --git a/properties/P000224.md b/properties/P000224.md
@@ -0,0 +1,17 @@
+---
+uid: P000224
+name: Weakly locally contractible
+refs:
+  - zb: "0087.38203"
+    name: On fiber spaces (Fadell)
+  - zb: "0642.54014"
+    name: LECS, local mixers, topological groups and special products (Borges)
+---
+
+Every point of $X$ has a neighborhood which is {P199}. 
+
+The name we have chosen for this property conforms to the [pi-base naming conventions](https://github.com/pi-base/data/wiki/Conventions-and-Style#Local-Properties).
+However, we have not seen this property mentioned with a specific name in the literature.
+
+The terminology "weakly locally contractible" has been used for multiple concepts different from this one, but the name is not standardized.
+A relatively common usage among those is as a synonym for "semilocally contractible" (see {{zb:0087.38203}} and {{zb:0642.54014}}).
diff --git a/properties/P000225.md b/properties/P000225.md
@@ -0,0 +1,26 @@
+---
+uid: P000225
+name: $LC$
+aliases:
+  - Locally contractible
+refs:
+  - zb: "0153.52905"
+    name: Theory of retracts (Borsuk)
+  - zb: "1280.54001"
+    name: Geometric aspects of general topology. (Sakai)
+  - zb: "1059.54001"
+    name: Encyclopedia of general topology
+---
+
+$X$ is *locally contractible at the point* $x$ for all $x \in X$,
+in the sense that every neighborhood $U$ of $x$ contains a neighborhood (equivalently, an open neighborhood) $V$ of $x$ that is contractible in $U$;
+i.e., such that the inclusion map $V \hookrightarrow U$ is null-homotopic.
+
+Equivalently, every neighborhood $U$ of any point $x$ contains a neighborhood (or an open neighborhood) $V$ of $x$
+such that the inclusion map $V \hookrightarrow U$ is homotopic to the constant map with value $x$.
+
+This is the standard definition of "locally contractible" in the theory of ANRs, as originally introduced by Borsuk. Defined as *locally contractible* on page 28 of {{zb:0153.52905}}, page 347 of {{zb:1280.54001}}, and page 341 of {{zb:1059.54001}}. The abbreviation $LC$ is commonly used in this context.
+
+----
+#### Meta-properties
+- This property is preserved by retractions (Theorem 15.3 on p. 28 of {{zb:0153.52905}}).
diff --git a/spaces/S000083/properties/P000216.md b/spaces/S000083/properties/P000216.md
@@ -4,4 +4,4 @@ property: P000216
 value: true
 ---
 
-Similar to the proof that {S83|P145}, using the fact that {S25|P216}.
+$X$ embeds as a subspace of {S209} and {S209|P216}.
diff --git a/spaces/S000107/properties/P000081.md b/spaces/S000107/properties/P000081.md
@@ -0,0 +1,10 @@
+---
+space: S000107
+property: P000081
+value: false
+refs:
+- mathse: 5132326
+  name: Answer to "Box topology on $\mathbb{R}^\omega$ is not Frechet-Urysohn"
+---
+
+See {{mathse:5132326}}.
diff --git a/spaces/S000107/properties/P000103.md b/spaces/S000107/properties/P000103.md
@@ -0,0 +1,10 @@
+---
+space: S000107
+property: P000103
+value: true
+refs:
+- mathse: 5132370
+  name: Is the countable box product of real lines $\mathbb{R}^\omega$ Strongly KC?
+---
+
+See {{mathse:5132370}}.
diff --git a/spaces/S000107/properties/P000206.md b/spaces/S000107/properties/P000206.md
@@ -0,0 +1,7 @@
+---
+space: S000107
+property: P000206
+value: true
+---
+
+Box product of {S25}, and {S25|P206}.
diff --git a/spaces/S000107/properties/P000234.md b/spaces/S000107/properties/P000234.md
@@ -1,10 +1,10 @@
 ---
 space: S000107
-property: P000041
+property: P000234
 value: false
 refs:
 - mathse: 5012784
   name: Answer to "Is $\ell^\infty$ with box topology connected?"
 ---
 
-By {{mathse:5012784}} the connected component of an arbitrary point $x\in X$ is $A = \{y : y_n = x_n\text{ for all but finitely many }n\}$. Since $\text{int}(A) = \emptyset$, it follows that $x$ has no connected neighbourhoods.
+By {{mathse:5012784}} the connected component of an arbitrary point $x\in X$ is $A = \{y : y_n = x_n\text{ for all but finitely many }n\}$. Since $\text{int}(A) = \emptyset$, it follows that $A$ is not open.
diff --git a/spaces/S000209/properties/P000068.md b/spaces/S000209/properties/P000068.md
@@ -0,0 +1,7 @@
+---
+space: S000209
+property: P000068
+value: false
+---
+
+Similar to {S83|P68}.
diff --git a/spaces/S000209/properties/P000216.md b/spaces/S000209/properties/P000216.md
@@ -0,0 +1,12 @@
+---
+space: S000209
+property: P000216
+value: true
+---
+
+It is enough to show that each open set in $X$ is {P30}.
+The whole space is {P30} since {S209|P16}.
+And a proper open subset of $X$ is a disjoint union of open sets,
+each homeomorphic to either {S170}, {S25} or {S83}.
+Observe each of {S170|P30}, {S25|P30} and {S83|P30}.
+Since the {P30} property is preserved by taking disjoint unions, the result follows.
diff --git a/spaces/S000220/properties/P000038.md b/spaces/S000220/properties/P000038.md
@@ -0,0 +1,7 @@
+---
+space: S000220
+property: P000038
+value: false
+---
+
+{S221} has a coarser topology than $X$, but {S221|P38}.
diff --git a/spaces/S000221/properties/P000038.md b/spaces/S000221/properties/P000038.md
@@ -0,0 +1,12 @@
+---
+space: S000221
+property: P000038
+value: false
+---
+
+Let $f:[0,1]\to X$ be a path in $X$.
+Take a countable dense subset $E$ of $[0,1]$.
+Its image $f(E)$ is countable and thus bounded in $X$, say by some $u\in\omega_1$.
+So $f(E)$ is contained in the closed set $[0,u]$.
+And by density of $E$ in $[0,1]$, $f([0,1])$ is also contained in $[0,u]$.
+Since $[0,u]$ is countable, $f$ cannot be injective.
diff --git a/theorems/T000391.md b/theorems/T000391.md
@@ -2,10 +2,10 @@
 uid: T000391
 if:
   and:
+    - P000163: true
     - P000058: false
-    - P000065: false
 then:
-  P000163: false
+  P000065: true
 ---
 
-Direct from the definitions.
+Immediate from the definitions.
diff --git a/theorems/T000847.md b/theorems/T000847.md
@@ -3,12 +3,8 @@ uid: T000847
 if:
   P000122: true
 then:
-  P000230: true
-refs:
-  - zb: "0951.54001"
-    name: Topology (Munkres)
+  P000223: true
 ---
 
-A locally Euclidean space admits a basis of Euclidean open balls.
-For a Euclidean open ball $U$ and $x \in U$, $\pi_1(U,x)$ is trivial (see Example 1 on page 331 of {{zb:0951.54001}}).
-A Euclidean open ball is also path-connected. 
+For each $x\in X$, every neighborhood of $x$ contains an open neighborhood homeomorphic to some Euclidean space $\mathbb R^n$.
+And $\mathbb R^n$ is {P199} as it can be deformation retracted to a point using a straight-line homotopy.
diff --git a/theorems/T000867.md b/theorems/T000867.md
@@ -0,0 +1,9 @@
+---
+uid: T000867
+if:
+  P000223: true
+then:
+  P000224: true
+---
+
+Immediate from the definitions.
diff --git a/theorems/T000868.md b/theorems/T000868.md
@@ -0,0 +1,9 @@
+---
+uid: T000868
+if:
+  P000223: true
+then:
+  P000225: true
+---
+
+Immediate from the definitions.
diff --git a/theorems/T000869.md b/theorems/T000869.md
@@ -0,0 +1,9 @@
+---
+uid: T000869
+if:
+  P000223: true
+then:
+  P000230: true
+---
+
+By {T583}.
diff --git a/theorems/T000870.md b/theorems/T000870.md
@@ -0,0 +1,9 @@
+---
+uid: T000870
+if:
+  P000224: true
+then:
+  P000231: true
+---
+
+By {T583}.
diff --git a/theorems/T000871.md b/theorems/T000871.md
@@ -0,0 +1,10 @@
+---
+uid: T000871
+if:
+  P000225: true
+then:
+  P000232: true
+---
+
+If $V$ is contractible in $U$, any map $Y \to V$ is null-homotopic in $U$.
+Apply this to $Y=S^0, S^1$.
diff --git a/theorems/T000872.md b/theorems/T000872.md
@@ -0,0 +1,9 @@
+---
+uid: T000872
+if:
+  P000199: true
+then:
+  P000224: true
+---
+
+Immediate from the definitions.

Original file line number	Diff line number	Diff line change
`@@ -18,3 +18,4 @@ Compare with {P38} and {P95}.`
`18`	`18`
`19`	`19`	`- $X$ satisfies this property iff its Kolmogorov quotient $\text{Kol}(X)$ does.`
`20`	`20`	`- This property is preserved by arbitrary products.`
	`21`	`+- This property is preserved in any coarser topology.`