diam_closedBall — Mathlib

English

The diameter of a closed ball is bounded by twice the radius: diam(closedBall x r) ≤ 2 r.

Русский

Диаметр замкнутого шара не превышает два радиуса: diam(закрытая шарa x r) ≤ 2r.

LaTeX

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

Lean4

theorem diam_closedBall {r : ℝ≥0∞} : diam (closedBall x r) ≤ 2 * r :=
  diam_le fun a ha b hb =>
    calc
      edist a b ≤ edist a x + edist b x := edist_triangle_right _ _ _
      _ ≤ r + r := (add_le_add ha hb)
      _ = 2 * r := (two_mul r).symm

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