Theorems · Definition · functional analysis

homeomorphUnitSphereProd

(E : Type u_1) → [inst : 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. See also homeomorphSphereProd for a version that works for a sphere of any positive radius.

Defined in

Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Cited by

8 results in Mathlib

Foundations

Depth 162 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace