no goals
ι : Sort ?u.149919
α✝ : Type u
β : Type v
inst✝² : PseudoEMetricSpace α✝
δ ε : ℝ
s t : Set α✝
x : α✝
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
E : Set α
hE : IsClosed E
hδ : 0 ≤ δ
⊢ cthickening δ E = ⋃ (x : α) (_ : x ∈ E), closedBall x δ
rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]