diam_thickening_le — Mathlib

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

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