Back to Project mathematical routes
A surjective isometry between unit spheres produces a radial map and transfers finite-dimensionality between the ambient spaces. The radial map has the recorded metric bounds; it is not asserted to be linear or globally isometric.
7 direct Cards + 0 reused prerequisites = 7 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: SR264 — A seminorm with two-sided bounds against a reference norm · SR272 — Continuous linear maps bounded by a seminorm · SR387 — Radial extension of an isometry between unit spheres · SR392 — The inverse sphere isometry gives the inverse radial map · SR394 — The radial extension is 3-Lipschitz · SR372 — Finite-dimensionality transfers across a sphere isometry · SR374 — Isometric unit spheres force equal finite dimensions
Reused prerequisites: None in this scope.
Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.
No Cards match this search. Clear search to recover this reading scope.
Extends a bijective sphere isometry to all vectors by retaining each radius and transporting its unit direction.
MathlibAnnex.Sphere.radialExtension
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The inverse sphere isometry gives the inverse radial map · The radial extension is 3-Lipschitz
Records a norm through a seminorm, two positive comparison constants and continuity on the original normed space.
MathlibAnnex.EquivalentSeminorm
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Continuous linear maps bounded by a seminorm
Defines the pointwise contraction condition relative to a stored equivalent seminorm.
MathlibAnnex.EquivalentSeminorm.IsContraction
Immediate Card prerequisites: A seminorm with two-sided bounds against a reference norm
Used by in this scope: None in this selected scope
Separates radial variation from the change of unit direction to obtain the global bound with coefficient 1 + 2.
MathlibAnnex.Sphere.lipschitzWith_radialExtension
Immediate Card prerequisites: Radial extension of an isometry between unit spheres
Used by in this scope: Finite-dimensionality transfers across a sphere isometry · Isometric unit spheres force equal finite dimensions
Shows that extending the inverse sphere isometry radially undoes the forward radial extension.
MathlibAnnex.Sphere.radialExtension_leftInverse
Immediate Card prerequisites: Radial extension of an isometry between unit spheres
Used by in this scope: Finite-dimensionality transfers across a sphere isometry · Isometric unit spheres force equal finite dimensions
Compares Hausdorff dimensions in both directions using the surjective Lipschitz radial maps.
MathlibAnnex.Sphere.finrank_eq
Immediate Card prerequisites: The inverse sphere isometry gives the inverse radial map · The radial extension is 3-Lipschitz
Used by in this scope: None in this selected scope
Uses the radial homeomorphism to transfer local compactness, then applies the finite-dimensionality criterion for real normed spaces.
MathlibAnnex.Sphere.finiteDimensional_codomain
Immediate Card prerequisites: The inverse sphere isometry gives the inverse radial map · The radial extension is 3-Lipschitz
Used by in this scope: None in this selected scope