Documentation

Mathlib.Analysis.NormedSpace.SphereNormEquiv

Homeomorphism between a normed space and sphere times (0, +∞) #

In this file we define a homeomorphism between nonzero elements of a normed space E and Metric.sphere (0 : E) 1 × Set.Ioi (0 : ℝ). One may think about it as generalization of polar coordinates to any normed space.

noncomputable def homeomorphUnitSphereProd (E : Type u_1) [NormedAddCommGroup E] [NormedSpace E] :
{0} ≃ₜ (Metric.sphere 0 1) × (Set.Ioi 0)

The natural homeomorphism between nonzero elements of a normed space E and Metric.sphere (0 : E) 1 × Set.Ioi (0 : ℝ).

The forward map sends ⟨x, hx⟩ to ⟨‖x‖⁻¹ • x, ‖x‖⟩, the inverse map sends (x, r) to r • x.

One may think about it as generalization of polar coordinates to any normed space.

Equations
  • One or more equations did not get rendered due to their size.
Instances For