dist_le_diam_of_mem — Mathlib

English

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

Русский

Если s ограничено и x,y ∈ s, то dist(x,y) ≤ diam(s).

LaTeX

$$$\\text{IsBounded}(s) \\Rightarrow (x \\in s \\land y \\in s) \\Rightarrow \\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 : IsBounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ diam s :=
  dist_le_diam_of_mem' h.ediam_ne_top hx hy

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