English
Sphere is path-connected in typical real vector spaces of dimension > 1.
Русский
Сфера в типичных вещественных векторных пространствах размерности > 1 путь-соединена.
LaTeX
$$$\\text{IsPathConnected}(\\text{sphere}(x,r))$ for $1<\\text{Module.rank}_\\mathbb{R} E$ and $r\\ge 0$$$
Lean4
/-- In a real vector space of dimension `> 1`, any sphere of nonnegative radius is
path connected. -/
theorem isPathConnected_sphere (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsPathConnected (sphere x r) :=
by
/- when `r > 0`, we write the sphere as the image of `{0}ᶜ` under the map
`y ↦ x + (r * ‖y‖⁻¹) • y`. Since the image under a continuous map of a path connected set
is path connected, this concludes the proof. -/
rcases hr.eq_or_lt with rfl | rpos
· simpa using isPathConnected_singleton x
let f : E → E := fun y ↦ x + (r * ‖y‖⁻¹) • y
have A : ContinuousOn f {0}ᶜ := by
intro y hy
apply (continuousAt_const.add _).continuousWithinAt
apply (continuousAt_const.mul (ContinuousAt.inv₀ continuousAt_id.norm ?_)).smul continuousAt_id
simpa using hy
have B : IsPathConnected ({0}ᶜ : Set E) := isPathConnected_compl_singleton_of_one_lt_rank h 0
have C : IsPathConnected (f '' {0}ᶜ) := B.image' A
have : f '' {0}ᶜ = sphere x r := by
apply Subset.antisymm
· rintro - ⟨y, hy, rfl⟩
have : ‖y‖ ≠ 0 := by simpa using hy
simp [f, norm_smul, abs_of_nonneg hr, mul_assoc, inv_mul_cancel₀ this]
· intro y hy
refine ⟨y - x, ?_, ?_⟩
· intro H
simp only [mem_singleton_iff, sub_eq_zero] at H
simp only [H, mem_sphere_iff_norm, sub_self, norm_zero] at hy
exact rpos.ne hy
· simp [f, mem_sphere_iff_norm.1 hy, mul_inv_cancel₀ rpos.ne']
rwa [this] at C
