volume_le_diam — Mathlib

English

For any set s ⊆ ℝ, the volume of s is at most its diameter: vol(s) ≤ diam(s).

Русский

Для любого множества s ⊆ ℝ объем vol(s) не превосходит диаметр diam(s).

LaTeX

$$$\operatorname{volume}(s) \le \operatorname{EMetric.diam}(s)$$$

Lean4

theorem volume_le_diam (s : Set ℝ) : volume s ≤ EMetric.diam s :=
  by
  by_cases hs : Bornology.IsBounded s
  · rw [Real.ediam_eq hs, ← volume_Icc]
    exact volume.mono hs.subset_Icc_sInf_sSup
  · rw [Metric.ediam_of_unbounded hs]; exact le_top

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