English
If E is compact and δ ≥ 0, then cthickening δ E equals the union over x in closure E of closedBall x δ.
Русский
Если E компактно, то δ-уплотнение E равно объединению по x в closure(E) замкнутых шаров радиуса δ.
LaTeX
$$$\operatorname{cthickening}_{\delta} E = \bigcup_{x\in \overline{E}} \overline{B}(x,δ)$$$
Lean4
/-- The closed thickening of a compact set `E` is the union of the balls `Metric.closedBall x δ`
over `x ∈ E`.
See also `Metric.cthickening_eq_biUnion_closedBall`. -/
theorem _root_.IsCompact.cthickening_eq_biUnion_closedBall {α : Type*} [PseudoMetricSpace α] {δ : ℝ} {E : Set α}
(hE : IsCompact E) (hδ : 0 ≤ δ) : cthickening δ E = ⋃ x ∈ E, closedBall x δ :=
by
rcases eq_empty_or_nonempty E with (rfl | hne)
· simp only [cthickening_empty, biUnion_empty]
refine Subset.antisymm (fun x hx ↦ ?_) (iUnion₂_subset fun x hx ↦ closedBall_subset_cthickening hx _)
obtain ⟨y, yE, hy⟩ : ∃ y ∈ E, infEdist x E = edist x y := hE.exists_infEdist_eq_edist hne _
have D1 : edist x y ≤ ENNReal.ofReal δ := (le_of_eq hy.symm).trans hx
have D2 : dist x y ≤ δ := by
rw [edist_dist] at D1
exact (ENNReal.ofReal_le_ofReal_iff hδ).1 D1
exact mem_biUnion yE D2
