Closedness, compactness, and the exact radius identity for successive closed-ball erosions.

theorem KamProject.Arnold1963.erosion_eq_iInter {E : Type u_1} [NormedAddCommGroup E] (U : Set E) (r : NNReal) : erosion U r = ⋂ v ∈ Metric.closedBall 0 ↑r, (fun (x : E) => x + v) ⁻¹' U

theorem KamProject.Arnold1963.isClosed_erosion {E : Type u_1} [NormedAddCommGroup E] {U : Set E} (hU : IsClosed U) (r : NNReal) : IsClosed (erosion U r)

theorem KamProject.Arnold1963.isCompact_erosion {E : Type u_1} [NormedAddCommGroup E] {U : Set E} (hU : IsCompact U) (r : NNReal) : IsCompact (erosion U r)

theorem KamProject.Arnold1963.erosion_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] (U : Set E) (r s : NNReal) : erosion (erosion U r) s = erosion U (r + s)