ball_contractible

Mathlib.Analysis.NormedSpace.Connected

URI: https://scilib.ai/kg/mathlib#Metric.ball_contractible

English

Balls are contractible subsets of normed spaces.

Русский

Шары —.Contractible подмножества нормированных пространств.

LaTeX

$$$\\text{ContractibleSpace}(\\text{ball}(x,r))$$$

Lean4

theorem ball_contractible {x : E} {r : ℝ} (hr : 0 < r) : ContractibleSpace (ball x r) :=
  Convex.contractibleSpace (convex_ball _ _) (by simpa)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru