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.

@[simp]

theorem homeomorphUnitSphereProd_apply_snd_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{0}ᶜ) : ↑((homeomorphUnitSphereProd E) x).2 = ‖↑x‖

@[simp]

theorem homeomorphUnitSphereProd_apply_fst_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑{0}ᶜ) : ↑((homeomorphUnitSphereProd E) x).1 = ‖↑x‖⁻¹ • ↑x

@[simp]

theorem homeomorphUnitSphereProd_symm_apply_coe (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)) : ↑((homeomorphUnitSphereProd E).symm x) = ↑x.2 • ↑x.1