LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The punctured disk is path-connected, locally path-connected and semilocally simply connected

Statement

Let $n \geq 0$ , let $D^{2} = {z \in C : ∣ z ∣ \leq 1}$ with the Euclidean subspace topology, let $Q_{n} \subseteq int D^{2}$ be the base configuration, and put $X = D^{2} ∖ Q_{n}$ . Then $X$ is nonempty and

(a) path-connected, (b) locally path-connected, (c) semilocally simply connected.

Explicitly, for every $x \in X$ there is an open neighbourhood $U$ of $x$ in $X$ that is convex as a subset of $R^{2}$ : if $∣ x ∣ < 1$ take $U = X \cap B (x, r)$ with $0 < r < \min ({∣ x - q_{i} ∣ : 1 \leq i \leq n} \cup {1 - ∣ x ∣}),$ an intersection of convex sets; if $∣ x ∣ = 1$ and $n \geq 1$ take $U = D^{2} \cap B (x, r)$ with $0 < r < \min_{1 \leq i \leq n} ∣ x - q_{i} ∣$ ; if $n = 0$ take $U = X = D^{2}$ . A nonempty convex subset of $R^{2}$ is path-connected and simply connected, so loops in $U$ are null-homotopic in $U$ , hence in $X$ (Every nonempty convex subset of $R^{n}$ is simply connected). No choice principle is used.

Facts & Assumptions

Given: $n \geq 0$ , the closed disk $D^{2}$ , the base configuration $Q_{n} = (q_{1}, \dots, q_{n}) \subseteq int D^{2}$ , the punctured disk $X = D^{2} ∖ Q_{n}$ with its subspace topology (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace), a point $x \in X$ , and the standard flower $W$ with its truncated tethers $t_{i}$ and circles $C_{i}$ (Standard meridians of a punctured disk).

[F1]

$W$ is a deformation retract of $X$ fixing the basepoint $d$ , with deformation retraction $(r, H)$ : $H : {id}_{X} ≃_{W} i \circ r$ is continuous with $H (a, 0) = a$ and $H (a, 1) = r (a)$ for all $a \in X$ (The standard flower is a deformation retract with free meridian basis, Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

[F2]

$W = {d} \cup ⋃_{i = 1}^{n} (t_{i} \cup C_{i})$ , and each $t_{i} \cup C_{i}$ meets ${d}$ in the tether endpoint $d$ ; a point of $t_{i}$ is joined to $d$ along $t_{i}$ , and a point of $C_{i}$ is joined to $d$ along $C_{i}$ to $p_{i}$ and then $t_{i}$ (Standard meridians of a punctured disk).

[F3]

Paths can be reversed and concatenated: $x \sim y$ iff $y \sim x$ , and $x \sim y$ , $y \sim z$ imply $x \sim z$ , with the reversed and concatenated paths continuous and taking values in the same subspace (Paths, path-connected spaces and path components).

[F4]

A subset of $R^{m}$ is convex when it contains every segment between two of its points; every convex subset is path-connected, and every Euclidean open ball $B (c, r) = {y : ∥ y - c ∥_{2} < r}$ is convex (A convex subset of $R^{m}$ contains every line segment between two of its points, Every convex subset of $R^{n}$ , in particular every ball and $R^{n}$ itself, is path-connected and hence connected, Euclidean spheres and closed balls as subspaces of $R^{n}$ , The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). By Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation(2), the Euclidean norm satisfies the norm axioms used below. The closed unit disk $D^{2}$ is convex: for $u, v \in D^{2}$ and $t \in [0, 1]$ , the triangle inequality and absolute homogeneity of the Euclidean norm give $∥ (1 - t) u + t v ∥_{2} \leq (1 - t) ∥ u ∥_{2} + t ∥ v ∥_{2} \leq 1$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F5]

Every nonempty convex subset $C \subseteq R^{m}$ , $m \geq 1$ , is simply connected: for every basepoint $x_{0} \in C$ and every loop $α$ at $x_{0}$ in $C$ , the straight-line formula $H (s, t) = (1 - t) α (s) + t x_{0}$ is a path homotopy in $C$ from $α$ to the constant loop (Every nonempty convex subset of $R^{n}$ is simply connected).

[F6]

$X$ is semilocally simply connected at $x$ when some neighbourhood $U$ of $x$ has the basepoint-preserving inclusion $(U, x) ↪ (X, x)$ inducing the trivial map on fundamental groups, and locally path-connected at $x$ when every open neighbourhood of $x$ contains an open path-connected neighbourhood of $x$ ; here a subset of $X$ is open when it is $X \cap V$ for an open $V \subseteq R^{2}$ (Semilocally simply connected spaces with explicit basepoint convention, Locally connected and locally path-connected spaces: a neighbourhood base of open connected, respectively open path-connected, sets at every point, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

Proof

technique · direct

1.1F1F2

Nonemptiness and paths to the flower. The point $d = (0, 1)$ lies in $X$ , because $∣ q_{i} ∣ < 1$ for every $i$ , so $X \neq \emptyset$ . By [F1] the map $γ_{a} (t) : = H (a, t)$ is a continuous path in $X$ from $a$ to $r (a) \in W$ for every $a \in X$ . The flower $W$ is path-connected: a point of $W$ lies in some $t_{i} \cup C_{i}$ or equals $d$ , and by [F2] it is joined to $d$ by a path inside $t_{i} \cup C_{i} \subseteq W$ , the case $W = {d}$ (that is, $n = 0$ ) being trivial.

1.2F4F6

Convex open neighbourhoods. Fix $x \in X$ . If $∣ x ∣ < 1$ , the minimum in the statement is over the nonempty set ${∣ x - q_{i} ∣} \cup {1 - ∣ x ∣}$ and is positive, since $x \neq q_{i}$ and $∣ x ∣ < 1$ ; fix $0 < r$ below it and put $U = X \cap B (x, r)$ . Then $B (x, r) \subseteq int D^{2} \subseteq D^{2}$ because $r < 1 - ∣ x ∣$ , and $q_{i} \notin B (x, r)$ for all $i$ because $r < ∣ x - q_{i} ∣$ ; hence $U = B (x, r)$ , an open ball. If $∣ x ∣ = 1$ and $n \geq 1$ , the finite minimum $\min_{i} ∣ x - q_{i} ∣$ is positive because $x \notin Q_{n}$ ; fix $0 < r$ below it and put $U = D^{2} \cap B (x, r)$ . Then $q_{i} \notin B (x, r)$ for all $i$ , so $U = X \cap B (x, r) \subseteq X$ . If $n = 0$ , put $U = X = D^{2}$ . In every case $x \in U \subseteq X$ , and $U = X \cap V$ with $V$ open in $R^{2}$ ( $V = B (x, r)$ , respectively $V = R^{2}$ for $U = X$ ), so $U$ is open in $X$ ; and $U$ is convex, being either an open ball, the intersection $D^{2} \cap B (x, r)$ of two convex sets, or $D^{2}$ .

2.1F3step 1.1

$X$ is path-connected. Let $a, b \in X$ . Concatenate the path $γ_{a}$ from $a$ to $r (a)$ , a path in $W$ from $r (a)$ to $d$ , the reverse of a path in $W$ from $r (b)$ to $d$ , and the reverse of $γ_{b}$ ; by [F3] the result is a path in $X$ from $a$ to $b$ . This uses only the finitely many explicit paths of step 1.1 and no choice principle.

2.2F4F5F6step 1.2

Local path-connectedness and semilocal simple connectivity. The set $U$ of step 1.2 is nonempty and convex, hence path-connected by [F4] and simply connected by [F5]; Given any open neighbourhood $O$ of $x$ in $X$ , the subspace topology supplies $r_{0} > 0$ with $X \cap B (x, r_{0}) \subseteq O$ . Further restrict the radius in step 1.2 to be below $r_{0}$ ; when $n = 0$ use $D^{2} \cap B (x, r_{0} / 2)$ instead of the whole disk. This remains convex and open, and gives a path-connected neighbourhood contained in $O$ . Thus these neighbourhoods form the required basis and $X$ is locally path-connected at $x$ . Moreover every loop in $U$ is null-homotopic in $U$ by the explicit straight-line homotopy of [F5], so the map $π_{1} (U, x) \to π_{1} (X, x)$ induced by the inclusion is trivial; by [F6] the space $X$ is semilocally simply connected at $x$ . Since $x \in X$ was arbitrary, (b) and (c) hold. No choice principle was used anywhere; all minima are over finite sets or over a finite set enlarged by one real number.

3.1step 1.1step 2.1step 2.2∎

Conclusion. Step 1.1 gives $X \neq \emptyset$ , step 2.1 gives (a), and step 2.2 gives (b) and (c); this is the assertion.

Depends on

Used by

The Burau infinite cyclic cover Definition
Braid mapping classes lift equivariantly to the Burau cover Lemma

Dependency tree · two levels

80 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Juan Gonzalez-Meneses, Basic results on braid groups, section 1.6 (printed pp. 8-10) and section 4 (Garside structure, printed pp. 26-30) (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, section 1.3 (covering spaces) and section 2.2 (cellular homology and its agreement with singular homology) (standard reference, not scraped)