convexHull_diam — Mathlib

English

The ordinary metric diameter of the convex hull equals the diameter of the original set.

Русский

Обычный диаметр выпуклой оболочки равен диаметрy исходного множества.

LaTeX

$$Metric.diam (convexHull ℝ s) = Metric.diam s$$

Lean4

/-- Diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
@[simp]
theorem convexHull_diam (s : Set E) : Metric.diam (convexHull ℝ s) = Metric.diam s := by
  simp only [Metric.diam, convexHull_ediam]

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