English
If hε ≥ 0 and hδ ≥ 0, then cthickening ε (ball x δ) = closedBall x (ε+δ).
Русский
Пусть ε ≥ 0 и δ ≥ 0. Тогда cthickening ε (ball x δ) = closedBall x (ε+δ).
LaTeX
$$$$\forall x:\; \operatorname{cthickening}(\varepsilon, \operatorname{ball}(x,\delta)) = \operatorname{closedBall}(x,\varepsilon+\delta), \quad \varepsilon\ge 0,\ \delta\ge 0.$$$$
Lean4
@[simp]
theorem cthickening_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) : cthickening ε (ball x δ) = closedBall x (ε + δ) := by
rw [← thickening_singleton, cthickening_thickening hε hδ, cthickening_singleton _ (add_nonneg hε hδ.le)]