English
There is a natural homeomorphism between the set of nonzero elements of a normed space E and the product sphere(0,1) × (0, ∞): x ↦ (‖x‖⁻¹ x, ‖x‖) with inverse (u, r) ↦ r u. It exhibits polar-type coordinates in normed spaces.
Русский
Существует естественный гомеоморфизм между множеством ненулевых элементов пространства E и произведением сферы и положительных вещественных: x ↦ (‖x‖⁻¹ x, ‖x‖) с обратным (u, r) ↦ r u.
LaTeX
$$homeomorph( {0}ᶜ, E ) ≃ₜ ( sphere(0,1) × Ioi(0) )$$
Lean4
/-- 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. -/
@[simps apply_fst_coe apply_snd_coe symm_apply_coe]
noncomputable def homeomorphUnitSphereProd : ({0}ᶜ : Set E) ≃ₜ (sphere (0 : E) 1 × Ioi (0 : ℝ))
where
toFun
x :=
(⟨‖x.1‖⁻¹ • x.1, by
rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ (norm_ne_zero_iff.2 x.2)]⟩,
⟨‖x.1‖, norm_pos_iff.2 x.2⟩)
invFun x := ⟨x.2.1 • x.1.1, smul_ne_zero x.2.2.out.ne' (ne_of_mem_sphere x.1.2 one_ne_zero)⟩
left_inv x := Subtype.eq <| by simp [smul_inv_smul₀ (norm_ne_zero_iff.2 x.2)]
right_inv
| (⟨x, hx⟩, ⟨r, hr⟩) => by
rw [mem_sphere_zero_iff_norm] at hx
rw [mem_Ioi] at hr
ext <;> simp [hx, norm_smul, abs_of_pos hr, hr.ne']
continuous_toFun := by
refine .prodMk (.codRestrict (.smul (.inv₀ ?_ ?_) ?_) _) ?_
· fun_prop
· simp
· fun_prop
· fun_prop
continuous_invFun := by apply Continuous.subtype_mk (by fun_prop)
