diam_closedBall

Mathlib.Topology.MetricSpace.Bounded

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

← MathLib Explorer

English

The diameter of a closed ball of radius r is at most 2r.

Русский

Диаметр замкнутой шара радиуса r не превосходит 2r.

LaTeX

$$$\\operatorname{diam}(\\overline{B}(x,r)) \\le 2r$$$

Lean4

/-- The diameter of a closed ball of radius `r` is at most `2 r`. -/
theorem diam_closedBall {r : ℝ} (h : 0 ≤ r) : diam (closedBall x r) ≤ 2 * r :=
  diam_le_of_subset_closedBall h Subset.rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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