dist_le_diam_of_mem' — Mathlib

English

If EMetric.diam(s) is finite and x,y ∈ s, then dist(x,y) ≤ diam(s).

Русский

Если э-медиация диаметра s конечна и x,y ∈ s, то dist(x,y) ≤ diam(s).

LaTeX

$$$\\text{If } \\operatorname{ediam}(s) \\neq \\infty \\text{ and } x,y \\in s, \\; \\operatorname{dist}(x,y) \\le \\operatorname{diam}(s)$$$

Lean4

/-- The distance between two points in a set is controlled by the diameter of the set. -/
theorem dist_le_diam_of_mem' (h : EMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s :=
  by
  rw [diam, dist_edist]
  exact ENNReal.toReal_mono h <| EMetric.edist_le_diam_of_mem hx hy

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