Theorems · Definition · functional analysis

homeomorphSphereProd

(E : Type u_2) →
  [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → (r : ℝ) → 0 < r → ↑{0}ᶜ ≃ₜ ↑(Metric.sphere 0 r) × ↑(Set.Ioi 0)

The natural homeomorphism between nonzero elements of a normed space E and Metric.sphere (0 : E) r × Set.Ioi (0 : ℝ), 0 < r. The forward map sends ⟨x, hx⟩ to ⟨r • ‖x‖⁻¹ • x, ‖x‖ / r⟩, the inverse map sends (x, r) to r • x. In the case of the unit sphere r = , one may think about it as generalization of polar coordinates to any normed space.

Defined in

Mathlib.Analysis.Normed.Module.Ball.RadialEquiv

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace