English
If s and t are disjoint, there exists δ > 0 such that the thickenings of s and t are still disjoint.
Русский
Если множества s и t не пересекаются, существует δ > 0 такое, что их утолщения остаются взаимно непересекающимися.
LaTeX
$$$\\exists \\delta > 0,\\ Disjoint(\\mathrm{thickening}_{\\delta}(s), \\mathrm{thickening}_{\\delta}(t)).$$$
Lean4
theorem _root_.Disjoint.exists_thickenings (hst : Disjoint s t) (hs : IsCompact s) (ht : IsClosed t) :
∃ δ, 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t) :=
by
obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst
refine ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩
rw [disjoint_iff_inf_le]
rintro z ⟨hzs, hzt⟩
rw [mem_thickening_iff_exists_edist_lt] at hzs hzt
rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt
obtain ⟨x, hx, hzx⟩ := hzs
obtain ⟨y, hy, hzy⟩ := hzt
refine (h x hx y hy).not_ge ?_
calc
edist x y ≤ edist z x + edist z y := edist_triangle_left _ _ _
_ ≤ ↑(r / 2) + ↑(r / 2) := (add_le_add hzx.le hzy.le)
_ = r := by rw [← ENNReal.coe_add, add_halves]
