ediam_le_of_forall_dist_le — Mathlib

English

If every pair of points in s is within distance ≤ C, then the emetric diameter satisfies ediam(s) ≤ ENNReal.ofReal(C).

Русский

Если для всех x,y ∈ s расстояние dist(x,y) ≤ C, то э-диаметр ediam(s) ≤ ENNReal.ofReal(C).

LaTeX

$$$\\forall x,y \\in s: \\operatorname{dist}(x,y) \\le C \\;\Rightarrow\\; \\operatorname{ediam}(s) \\le \\operatorname{ENNReal.ofReal}(C)$$$

Lean4

/-- If the distance between any two points in a set is bounded by some constant `C`,
then `ENNReal.ofReal C` bounds the emetric diameter of this set. -/
theorem ediam_le_of_forall_dist_le {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : EMetric.diam s ≤ ENNReal.ofReal C :=
  EMetric.diam_le fun x hx y hy => (edist_dist x y).symm ▸ ENNReal.ofReal_le_ofReal (h x hx y hy)

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