exists_cthickening_subset_open — Mathlib

English

For a set s and ε ≥ 0, the diameter of the thickening is bounded by the original diameter plus 2ε: diam(thickening ε s) ≤ diam s + 2ε.

Русский

Для множества s и ε ≥ 0 диаметр утолщения ограничен диаметром s плюс 2ε.

LaTeX

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

Lean4

/-- If `s` is compact, `t` is open and `s ⊆ t`, some `cthickening` of `s` is contained in `t`. -/
theorem _root_.IsCompact.exists_cthickening_subset_open (hs : IsCompact s) (ht : IsOpen t) (hst : s ⊆ t) :
    ∃ δ, 0 < δ ∧ cthickening δ s ⊆ t :=
  (hst.disjoint_compl_right.exists_cthickenings hs ht.isClosed_compl).imp fun _ h =>
    ⟨h.1, disjoint_compl_right_iff_subset.1 <| h.2.mono_right <| self_subset_cthickening _⟩

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