exists_cthickenings — Mathlib

English

If s and t are disjoint, there exists δ > 0 such that the cthickening of s and the cthickening of t are disjoint.

Русский

Если s и t не пересекаются, существует δ > 0 такое, что cthickening δ(s) и cthickening δ(t) не пересекаются.

LaTeX

$$$\\exists \\delta > 0,\\ \\mathrm{Disjoint}(\\mathrm{cthickening}_{\\delta}(s), \\mathrm{cthickening}_{\\delta}(t)).$$$

Lean4

theorem _root_.Disjoint.exists_cthickenings (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) :
    ∃ δ, 0 < δ ∧ Disjoint (cthickening δ s) (cthickening δ t) :=
  by
  obtain ⟨δ, hδ, h⟩ := hst.exists_thickenings hs ht
  refine ⟨δ / 2, half_pos hδ, h.mono ?_ ?_⟩ <;> exact cthickening_subset_thickening' hδ (half_lt_self hδ) _

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