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.

Alexander trick: a sphere homeomorphism extends radially over the disk

Statement

Let $d \geq 1$ and let $f : S^{d - 1} \to S^{d - 1}$ be a homeomorphism of the unit sphere $S^{d - 1} \subseteq R^{d}$ . Then $f$ extends to a homeomorphism $F : D^{d} \to D^{d}$ of the closed unit disk, given by $F (0) = 0, F (r x) = r f (x) for 0 < r \leq 1, x \in S^{d - 1} .$ The extension need not be smooth at the origin.

Facts & Assumptions

Given: An integer $d \geq 1$ , a homeomorphism $f : S^{d - 1} \to S^{d - 1}$ , and the closed unit disk $D^{d} : = {\overline{B}}_{2} (0, 1) \subseteq R^{d}$ with its Euclidean norm $∥ \cdot ∥ = ∥ \cdot ∥_{2}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[F1]

The boundary map $f$ is a homeomorphism of $S^{d - 1}$ ; hence it maps $S^{d - 1}$ into itself, so $∥ f (x) ∥ = 1$ for every $x \in S^{d - 1}$ , and both $f$ and its inverse $f^{- 1}$ are continuous (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[L1]

For every scalar $λ$ and every $v \in R^{d}$ one has $∥ λ v ∥ = ∣ λ ∣ ∥ v ∥$ , and $∥ x ∥ = 1$ exactly when $x \in S^{d - 1}$ (Inner products separate vectors, and the induced norm is homogeneous: $∥ λ v ∥ = ∣ λ ∣ ∥ v ∥$ ).

[L2]

For all $u, w \in R^{d}$ one has $∣ ∥ u ∥ - ∥ w ∥ ∣ \leq ∥ u - w ∥$ (The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ ).

[L3]

The radial normalisation $ρ : R^{d} ∖ {0} \to S^{d - 1}$ , $ρ (y) = y / ∥ y ∥$ , is continuous, and $D^{d} = {y \in R^{d} : ∥ y ∥ \leq 1}$ (Radial normalisation $x \mapsto x / ∥ x ∥_{2}$ is continuous on $R^{n} ∖ {0}$ , Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

Proof

technique · direct

1.1F1L1L3given

Every $y \in D^{d} ∖ {0}$ has a unique representation $y = r x$ with $0 < r \leq 1$ and $x \in S^{d - 1}$ , namely $r = ∥ y ∥$ and $x = ρ (y)$ : taking norms in $y = r x$ gives $r = ∥ y ∥$ by [L1], and dividing by that positive number gives $x = ρ (y)$ ; conversely $∥ y ∥ \leq 1$ and $ρ (y) \in S^{d - 1}$ by [L3], so this pair is admissible, and in particular the prescription of the statement defines a function $F$ on $D^{d}$ .

2.1step 1.1F1L1

For $r \in (0, 1]$ and $x \in S^{d - 1}$ one has $∥ F (r x) ∥ = ∥ r f (x) ∥ = r ∥ f (x) ∥ = r \leq 1$ by [F1] and [L1], so $F$ maps $D^{d}$ into $D^{d}$ , and $F (0) = 0$ lies in $D^{d}$ .

3.1step 1.1step 2.1F1given

Define $G : D^{d} \to D^{d}$ by $G (0) = 0$ and $G (r y) = r f^{- 1} (y)$ for $0 < r \leq 1$ , $y \in S^{d - 1}$ , which is a function by the same argument as step 1.1 with $f$ replaced by $f^{- 1}$ ; then $G (F (r x)) = G (r f (x)) = r f^{- 1} (f (x)) = r x$ and $F (G (r y)) = F (r f^{- 1} (y)) = r f (f^{- 1} (y)) = r y$ for all $r \in (0, 1]$ and $x, y \in S^{d - 1}$ , while both composites fix $0$ , so $G \circ F = {i d}_{D^{d}}$ and $F \circ G = {i d}_{D^{d}}$ and $F$ is a bijection with inverse $G$ .

3.2step 2.1L1

Continuity of $F$ at $0$ : every $ε > 0$ satisfies $∥ F (y) - F (0) ∥ = ∥ F (y) ∥ = ∥ y ∥ < ε$ whenever $∥ y - 0 ∥ < ε$ by [L1] and step 2.1, so $F$ is continuous at $0$ .

3.3step 1.1step 2.1F1L1L2L3

Continuity of $F$ at a point $y_{0} \neq 0$ : writing $r = ∥ y ∥$ , $r_{0} = ∥ y_{0} ∥$ , $x = ρ (y)$ , $x_{0} = ρ (y_{0})$ for $y \neq 0$ gives $F (y) - F (y_{0}) = r (f (x) - f (x_{0})) + (r - r_{0}) f (x_{0})$ by [L1] and bilinearity, hence $∥ F (y) - F (y_{0}) ∥ \leq ∥ f (x) - f (x_{0}) ∥ + ∥ y - y_{0} ∥$ because $r \leq 1$ , because $∥ f (x_{0}) ∥ = 1$ by [F1], and because $∣ r - r_{0} ∣ \leq ∥ y - y_{0} ∥$ by [L2]; given $ε > 0$ , continuity of $f$ at $x_{0}$ gives $η > 0$ with $∥ f (x) - f (x_{0}) ∥ < ε / 2$ whenever $∥ x - x_{0} ∥ < η$ , and continuity of $ρ$ at $y_{0}$ ([L3]) gives $δ > 0$ with $∥ ρ (y) - ρ (y_{0}) ∥ < η$ and $∥ y - y_{0} ∥ < ε / 2$ whenever $0 < ∥ y - y_{0} ∥ < δ$ , so $∥ F (y) - F (y_{0}) ∥ < ε$ for all such $y$ and $F$ is continuous at $y_{0}$ .

4.1step 3.1step 3.2step 3.3F1given

The arguments of steps 3.2 and 3.3 used only that the boundary map is a continuous map $S^{d - 1} \to S^{d - 1}$ and that its values lie in $S^{d - 1}$ ; applying them with $f$ replaced by the continuous map $f^{- 1}$ of [F1] shows that the inverse $G$ of step 3.1 is continuous on $D^{d}$ .

5.1step 3.1step 3.2step 3.3step 4.1∎

Therefore $F : D^{d} \to D^{d}$ is a continuous bijection with continuous inverse $G$ , that is a homeomorphism, and it restricts to $f$ on $S^{d - 1}$ because $F (1 \cdot x) = f (x)$ for $x \in S^{d - 1}$ , which proves the extension claim.

Remarks

Why smoothness can fail. Suppose $F$ is differentiable at $0$ with derivative $A$ (in the sense of the derivative as a linear map). For every $x \in S^{d - 1}$ and every $t \in (0, 1]$ one has $F (t x) = t f (x)$ , so $\frac{∥ F (t x) - A (t x) ∥}{t} = ∥ f (x) - A x ∥ \to_{t \to 0^{+}}^{} 0,$ and therefore $f (x) = A x$ : the boundary map is itself the restriction of the linear map $A$ . Consequently, for a homeomorphism $f$ of $S^{d - 1}$ that is not the restriction of a linear map, the radial extension $F$ is not differentiable at the origin and in particular is not smooth there. Such homeomorphisms exist for every $d \geq 2$ : for $0 < ε < 1$ the map $θ \mapsto θ + ε \sin θ$ is strictly increasing (its derivative $1 + ε \cos θ$ is positive) and commutes with translation by $2 π$ , so it descends to a homeomorphism $f_{ε}$ of the circle $S^{1}$ , and $f_{ε}$ is a rotation or a reflection only for $ε = 0$ . For $d > 2$ , write a sphere point as $(r \cos θ, r \sin θ, z)$ with $z \in R^{d - 2}$ and apply this angular map to $θ$ , leaving $r, z$ fixed. At $r = 0$ the map and its inverse extend continuously because the first two coordinates have norm $r$ ; on $z = 0$ it is the same nonlinear circle map, so it cannot be the restriction of a linear map. Thus the extension is not automatically smooth at the origin, which is why it is used only as a topological gluing map in the applications below. Milnor's treatment of the two-disk argument likewise uses the radial extension as a homeomorphism only (Milnor, Lectures on the h-Cobordism Theorem, section 9, printed pp. 109-110).

Depends on

Used by

The Milnor homotopy seven-spheres are homeomorphic to S⁷ Corollary

Dependency tree · two levels

37 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

John Milnor, Lectures on the h-Cobordism Theorem, section 9, printed pp. 109-110 (standard reference, not scraped)