diam_ball

Mathlib.Topology.EMetricSpace.Diam

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

English

The diameter of a ball is at most twice its radius: diam(ball x r) ≤ 2 r.

Русский

Диаметр открытой или любой шаровой области не превосходит двойного радиуса: diam(ball x r) ≤ 2r.

LaTeX

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

Lean4

theorem diam_ball {r : ℝ≥0∞} : diam (ball x r) ≤ 2 * r :=
  le_trans (diam_mono ball_subset_closedBall) diam_closedBall

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

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

Разделы

Аффилиация

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