isBounded_iff_ediam_ne_top — Mathlib

English

A set is bounded if and only if its emetric diameter is finite.

Русский

Множество ограничено тогда и только тогда, когда его эметрический диаметр конечен.

LaTeX

$$$\\operatorname{IsBounded}(s) \\iff \\operatorname{ediam}(s) \\neq \\infty$$$

Lean4

/-- Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter. -/
theorem isBounded_iff_ediam_ne_top : IsBounded s ↔ EMetric.diam s ≠ ⊤ :=
  isBounded_iff.trans <|
    Iff.intro (fun ⟨_C, hC⟩ => ne_top_of_le_ne_top ENNReal.ofReal_ne_top <| ediam_le_of_forall_dist_le hC) fun h =>
      ⟨diam s, fun _x hx _y hy => dist_le_diam_of_mem' h hx hy⟩

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