diam_le_of_subset_closedBall — Mathlib

English

If s ⊆ closedBall x r and r ≥ 0, then diam s ≤ 2r.

Русский

Если s ⊆ замкнутая шаровая оболочка с центром x и радиусом r, то diam s ≤ 2r.

LaTeX

$$$0 \\le r \\Rightarrow s \\subseteq \\overline{B}(x,r) \\Rightarrow \\operatorname{diam}(s) \\le 2r$$$

Lean4

theorem diam_le_of_subset_closedBall {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ closedBall x r) : diam s ≤ 2 * r :=
  diam_le_of_forall_dist_le (mul_nonneg zero_le_two hr) fun a ha b hb =>
    calc
      dist a b ≤ dist a x + dist b x := dist_triangle_right _ _ _
      _ ≤ r + r := (add_le_add (h ha) (h hb))
      _ = 2 * r := by simp [mul_two, mul_comm]

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