diam_le_of_forall_dist_le — Mathlib

English

If there exists a nonnegative real C such that dist(x,y) ≤ C for all x,y ∈ s, then diam(s) ≤ C.

Русский

Если существует неотрицательное вещественное C, такое что dist(x,y) ≤ C для всех x,y ∈ s, то diam(s) ≤ C.

LaTeX

$$$0 \\le C \\land \\forall x\\in s, \\forall y\\in s:\\ \\operatorname{dist}(x,y) \\le C \\Rightarrow \\operatorname{diam}(s) \\le C$$$

Lean4

/-- If the distance between any two points in a set is bounded by some non-negative constant,
this constant bounds the diameter. -/
theorem diam_le_of_forall_dist_le {C : ℝ} (h₀ : 0 ≤ C) (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) : diam s ≤ C :=
  ENNReal.toReal_le_of_le_ofReal h₀ (ediam_le_of_forall_dist_le h)

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