isPreconnected_sphere — Mathlib

English

Spheres are preconnected in higher dimensions.

Русский

Сферы предсоединены в пространствах большей размерности.

LaTeX

$$$\\text{IsPreconnected}(\\text{sphere}(x,r))$ for $1<\\dim E$$$

Lean4

/-- In a real vector space of dimension `> 1`, any sphere is preconnected. -/
theorem isPreconnected_sphere (h : 1 < Module.rank ℝ E) (x : E) (r : ℝ) : IsPreconnected (sphere x r) :=
  by
  rcases le_or_gt 0 r with hr | hr
  · exact (isConnected_sphere h x hr).isPreconnected
  · simpa [hr] using isPreconnected_empty

Похожие утверждения