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.
Euclidean spheres and closed balls as subspaces of
Definition
Let with . Give its Euclidean norm and its induced Euclidean metric ( as the set of functions , and , , are metrics on it, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). For and , put
These are respectively the Euclidean closed ball and Euclidean sphere with centre and radius . They carry the subspace topology inherited from (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). Since , they are precisely the closed ball and sphere and of the metric-space definition (Open ball, closed ball and sphere in a metric space).
For the unit sphere centred at the origin write
The exponent is notation for this particular sphere, not a claim that a dimension theory has been developed here.
Depends on
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- 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
- Open ball, closed ball and sphere in a metric space
- $\mathbb{R}^n$ as the set of functions $n \to \mathbb{R}$, and $d_1$, $d_2$, $d_\infty$ are metrics on it
Used by
- For n≥1, every Euclidean closed ball and every Euclidean sphere of positive radius is compact Corollary
- For n≥2, the sphere Sⁿ⁻¹ is path-connected and connected Corollary
- The Euclidean closed ball and sphere worked through the compactness equivalence chart Example
- Radial normalisation x↦ x/‖ x‖₂ is continuous on ℝⁿ∖{0} Lemma
- 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: 87 results over 19 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
- Euclidean space (standard reference, not scraped)
- Sphere (standard reference, not scraped)