isConnected_sphere — Mathlib

English

Sphere is connected in higher dimensions.

Русский

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

LaTeX

$$$\\text{IsConnected}(\\text{sphere}(x,r))$ for $1<\\dim E$ and $r\\ge 0$$$

Lean4

/-- In a real vector space of dimension `> 1`, any sphere of nonnegative radius is connected. -/
theorem isConnected_sphere (h : 1 < Module.rank ℝ E) (x : E) {r : ℝ} (hr : 0 ≤ r) : IsConnected (sphere x r) :=
  (isPathConnected_sphere h x hr).isConnected

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