English
If hε > 0 and hδ > 0, then thickening ε (ball x δ) = ball x (ε + δ).
Русский
Если ε > 0 и δ > 0, то thickening ε (ball x δ) = ball x (ε + δ).
LaTeX
$$$$\forall x\in E:\; \operatorname{thickening}(\varepsilon, \operatorname{ball}(x,\delta)) = \operatorname{ball}(x, \varepsilon+\delta), \quad \varepsilon>0,\ \delta>0.$$$$
Lean4
@[simp]
theorem thickening_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (x : E) : thickening ε (closedBall x δ) = ball x (ε + δ) := by
rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]