diam_pos — Mathlib

English

If a set s is nonempty and bounded, then its diameter is positive.

Русский

Если множество s непусто и ограничено, то его диаметр положителен.

LaTeX

$$$s.nonempty \Rightarrow s.\operatorname{diam} > 0$ (under the assumption \text{IsBounded}(s)).$$

Lean4

theorem diam_pos [MetricSpace α] (hs1 : s.Nontrivial) (hs2 : IsBounded s) : 0 < diam s :=
  by
  rcases hs1 with ⟨x, hx, y, hy, hxy⟩
  exact (dist_pos.mpr hxy).trans_le <| Metric.dist_le_diam_of_mem hs2 hx hy

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