diam_le_of_forall_dist_le_of_nonempty

English

If s is nonempty and dist(x,y) ≤ C for all x,y ∈ s, then diam(s) ≤ C.

Русский

Если s непусто и для всех x,y ∈ s выполнено dist(x,y) ≤ C, то diam(s) ≤ C.

LaTeX

$$$s \\neq \\varnothing \\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 nonempty set is bounded by some constant,
this constant bounds the diameter. -/
theorem diam_le_of_forall_dist_le_of_nonempty (hs : s.Nonempty) {C : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) :
    diam s ≤ C :=
  have h₀ : 0 ≤ C :=
    let ⟨x, hx⟩ := hs
    le_trans dist_nonneg (h x hx x hx)
  diam_le_of_forall_dist_le h₀ h

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