English
Thickening commutes with closure: thickening δ (closure E) = thickening δ E.
Русский
Утолщение коммутирует с замыканием: thickening δ (closure E) = thickening δ E.
LaTeX
$$$\\mathrm{thickening}_{\\delta}(\\overline{E}) = \\mathrm{thickening}_{\\delta}(E).$$$
Lean4
theorem diam_thickening_le {α : Type*} [PseudoMetricSpace α] (s : Set α) (hε : 0 ≤ ε) :
diam (thickening ε s) ≤ diam s + 2 * ε := by
by_cases hs : IsBounded s
· exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans (diam_cthickening_le _ hε)
obtain rfl | hε := hε.eq_or_lt
· simp [thickening_of_nonpos, diam_nonneg]
· rw [diam_eq_zero_of_unbounded (mt (IsBounded.subset · <| self_subset_thickening hε _) hs)]
positivity