English
For a metric space, δ>0 and δ' with δ < δ', the δ-thickening of E is contained in the union over x∈E of closed balls of radius δ' centered at x.
Русский
При δ'>δ>0 уплотнение δE ⊆ ⋃_{x∈E}
{ closedBall(x,δ') }.
LaTeX
$$$\operatorname{cthickening}_{\delta} E \subseteq \bigcup_{x\in E} \overline{B}(x,δ')$ for 0<δ' and δ<δ'.$$
Lean4
theorem cthickening_subset_iUnion_closedBall_of_lt {α : Type*} [PseudoMetricSpace α] (E : Set α) {δ δ' : ℝ}
(hδ₀ : 0 < δ') (hδδ' : δ < δ') : cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ' :=
by
refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_
obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx
exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩