isConnected_eball — Mathlib

English

Spheres of nonnegative radius are path-connected in higher dimensions.

Русский

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

LaTeX

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

Lean4

theorem isConnected_eball {x : E} {r : ENNReal} (hr : 0 < r) : IsConnected (EMetric.ball x r) :=
  (isPathConnected_eball hr).isConnected

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