English
If E is closed, then cthickening δ E equals the union over x ∈ E of closedBall x δ.
Русский
Если E замкнуто, то δ-уплотнение E равно объединению замкнутых шаров по x ∈ E радиуса δ.
LaTeX
$$$\operatorname{cthickening}_{\delta} E = \bigcup_{x\in E} \overline{B}(x,δ)$$$
Lean4
theorem cthickening_eq_biUnion_closedBall {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (E : Set α) (hδ : 0 ≤ δ) :
cthickening δ E = ⋃ x ∈ closure E, closedBall x δ :=
by
rcases eq_empty_or_nonempty E with (rfl | hne)
· simp only [cthickening_empty, biUnion_empty, closure_empty]
rw [← cthickening_closure]
refine Subset.antisymm (fun x hx ↦ ?_) (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
obtain ⟨y, yE, hy⟩ : ∃ y ∈ closure E, infDist x (closure E) = dist x y :=
isClosed_closure.exists_infDist_eq_dist (closure_nonempty_iff.mpr hne) x
replace hy : dist x y ≤ δ :=
(ENNReal.ofReal_le_ofReal_iff hδ).mp
(((congr_arg ENNReal.ofReal hy.symm).le.trans ENNReal.ofReal_toReal_le).trans hx)
exact mem_biUnion yE hy
