English
The emetric diameter of the convex hull equals the emetric diameter of the set.
Русский
Эм-диаметр выпуклой оболочки равен эм-диаметру множества.
LaTeX
$$EMetric.diam (convexHull ℝ s) = EMetric.diam s$$
Lean4
/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s`. -/
@[simp]
theorem convexHull_ediam (s : Set E) : EMetric.diam (convexHull ℝ s) = EMetric.diam s :=
by
refine (EMetric.diam_le fun x hx y hy => ?_).antisymm (EMetric.diam_mono <| subset_convexHull ℝ s)
rcases convexHull_exists_dist_ge2 hx hy with ⟨x', hx', y', hy', H⟩
rw [edist_dist]
apply le_trans (ENNReal.ofReal_le_ofReal H)
rw [← edist_dist]
exact EMetric.edist_le_diam_of_mem hx' hy'
