diam_ball

Mathlib.Topology.MetricSpace.Bounded

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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