Alphabeta MathHow 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.
Radial normalisation is continuous on
Statement
For , the map defined by is continuous.
Facts & Assumptions
Given: , the Euclidean norm, and a nonzero point .
The Euclidean norm is continuous and satisfies (The finite and reverse triangle inequalities for a norm; and for every norm on satisfies and is Lipschitz, hence continuous, for ).
Componentwise continuity gives continuity into (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Vector-valued functions , their limits and continuity, with the dictionary to the metric notions); and a map into a subspace is continuous exactly when its composite with the ambient inclusion is continuous, so a continuous map whose image lies in the subspace is continuous into it (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).
The unit sphere is the set of vectors with Euclidean norm (Euclidean spheres and closed balls as subspaces of ).
Proof
Put . If , then [L1] gives .
For such , .
Step 1.2 gives the epsilon-delta condition at , so is continuous on the punctured space. Also , so its image lies in and [L2] gives continuity with that codomain.
Depends on
- Vector-valued functions $f : A \to \mathbb{R}^m$, their limits and continuity, with the dictionary to the metric notions
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$
- Euclidean spheres and closed balls as subspaces of $\mathbb{R}^n$
- 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
Used by
- For n≥2, the sphere Sⁿ⁻¹ is path-connected and connected Corollary
- For n≥1, radial normalisation is a deformation retraction of ℝⁿ∖{0} onto Sⁿ⁻¹ Theorem
- For n≥1, the map H(x,t)=((1-t)+t/‖ x‖₂)x is continuous on (ℝⁿ∖{0})×[0,1], starts at x, ends at radial normalisation, fixes the unit sphere, and never reaches 0 Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 141 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Sphere (standard reference, not scraped)
- Deformation retract (standard reference, not scraped)