English
For ε ≥ 0, the diameter of the closed thickening is bounded by the diameter of the original set plus 2ε: ediam(cthickening ε s) ≤ ediam s + 2ε.
Русский
При ε ≥ 0 диагаметр закрытого утолщения ограничен диагаметром исходного множества плюс 2ε: ediam(cthickening ε s) ≤ ediam s + 2ε.
LaTeX
$$$\\operatorname{ediam}\\bigl(\\mathrm{cthickening}_{\\epsilon} s\\bigr) \\le \\operatorname{ediam}(s) + 2 \\epsilon \\quad(\\epsilon \\ge 0).$$$
Lean4
theorem ediam_cthickening_le (ε : ℝ≥0) : EMetric.diam (cthickening ε s) ≤ EMetric.diam s + 2 * ε :=
by
refine diam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => ?_
rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy
have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
replace hx := hx.trans_lt hε
obtain ⟨x', hx', hxx'⟩ := infEdist_lt_iff.mp hx
calc
edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
_ ≤ ε + δ + (infEdist y s + EMetric.diam s) := (add_le_add hxx'.le (edist_le_infEdist_add_ediam hx'))
_ ≤ ε + δ + (ε + EMetric.diam s) := by grw [hy]
_ = _ := by rw [two_mul]; ac_rfl
