ediam_thickening_le — Mathlib

English

For ε ≥ 0, the diameter bound holds for thickening: ediam(thickening ε s) ≤ ediam s + 2ε.

Русский

Для ε ≥ 0 верно ограничение на диаметр для утолщения: ediam(thickening ε s) ≤ ediam s + 2ε.

LaTeX

$$$\\operatorname{ediam}\\bigl(\\mathrm{thickening}_{\\varepsilon} s\\bigr) \\le \\operatorname{ediam}(s) + 2\\varepsilon \\quad(\\varepsilon \\ge 0).$$$

Lean4

theorem ediam_thickening_le (ε : ℝ≥0) : EMetric.diam (thickening ε s) ≤ EMetric.diam s + 2 * ε :=
  (EMetric.diam_mono <| thickening_subset_cthickening _ _).trans <| ediam_cthickening_le _

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