diam_cthickening_le — Mathlib

English

For ε ≥ 0, the diameter of the δ-thickening does not exceed the diameter plus 2ε: diam(cthickening ε s) ≤ diam s + 2ε.

Русский

При ε ≥ 0 диаметр ct-thickening не превышает диагаметр s плюс 2ε: diam(cthickening ε s) ≤ diam s + 2ε.

LaTeX

$$$\\operatorname{diam}(\\mathrm{cthickening}_{\\varepsilon}(s)) \\le \\operatorname{diam}(s) + 2\\varepsilon \\quad(\\varepsilon \\ge 0).$$$

Lean4

theorem diam_cthickening_le {α : Type*} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) :
    diam (cthickening ε s) ≤ diam s + 2 * ε := by
  lift ε to ℝ≥0 using hε
  refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
  · exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (self_subset_cthickening _)
  · simp [mul_eq_top]
  · simp [diam]

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