thickening_closedBall — Mathlib

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]

Похожие утверждения